Trivial submodule is a trivial subrepresentation

Stream: FLT

[Stepan Nesterov]

How to prove the following statement:

example {R : Type*} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (V : Type*) [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V]
    {ρ : GaloisRep ℚ R V}
    (U : Subrepresentation ρ.toRepresentation) : U.toSubmodule = ⊥ → U = ⊥ := by sorry

[Kenny Lau]

@Stepan Nesterov I don't have FLT open, but try to replace by sorry by fun h ↦ Subrepresentation.toSubmodule_injective h (remember the by needs to go)