Metamath Proof Explorer

Theorem lmhmima

Description: The image of a subspace under a homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmima.x ⊢ X = LSubSp ⁡ S
lmhmima.y ⊢ Y = LSubSp ⁡ T
Assertion lmhmima ⊢ F ∈ S LMHom T ∧ U ∈ X → F U ∈ Y

Proof

Step Hyp Ref Expression
1 lmhmima.x ⊢ X = LSubSp ⁡ S
2 lmhmima.y ⊢ Y = LSubSp ⁡ T
3 lmghm ⊢ F ∈ S LMHom T → F ∈ S GrpHom T
4 lmhmlmod1 ⊢ F ∈ S LMHom T → S ∈ LMod
5 simpr ⊢ F ∈ S LMHom T ∧ U ∈ X → U ∈ X
6 1 lsssubg ⊢ S ∈ LMod ∧ U ∈ X → U ∈ SubGrp ⁡ S
7 4 5 6 syl2an2r ⊢ F ∈ S LMHom T ∧ U ∈ X → U ∈ SubGrp ⁡ S
8 ghmima ⊢ F ∈ S GrpHom T ∧ U ∈ SubGrp ⁡ S → F U ∈ SubGrp ⁡ T
9 3 7 8 syl2an2r ⊢ F ∈ S LMHom T ∧ U ∈ X → F U ∈ SubGrp ⁡ T
10 eqid ⊢ Base S = Base S
11 eqid ⊢ Base T = Base T
12 10 11 lmhmf ⊢ F ∈ S LMHom T → F : Base S ⟶ Base T
13 12 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X → F : Base S ⟶ Base T
14 ffn ⊢ F : Base S ⟶ Base T → F Fn Base S
15 13 14 syl ⊢ F ∈ S LMHom T ∧ U ∈ X → F Fn Base S
16 10 1 lssss ⊢ U ∈ X → U ⊆ Base S
17 5 16 syl ⊢ F ∈ S LMHom T ∧ U ∈ X → U ⊆ Base S
18 15 17 fvelimabd ⊢ F ∈ S LMHom T ∧ U ∈ X → b ∈ F U ↔ ∃ c ∈ U F ⁡ c = b
19 18 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T → b ∈ F U ↔ ∃ c ∈ U F ⁡ c = b
20 simpll ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → F ∈ S LMHom T
21 eqid ⊢ Scalar ⁡ S = Scalar ⁡ S
22 eqid ⊢ Scalar ⁡ T = Scalar ⁡ T
23 21 22 lmhmsca ⊢ F ∈ S LMHom T → Scalar ⁡ T = Scalar ⁡ S
24 23 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X → Scalar ⁡ T = Scalar ⁡ S
25 24 fveq2d ⊢ F ∈ S LMHom T ∧ U ∈ X → Base Scalar ⁡ T = Base Scalar ⁡ S
26 25 eleq2d ⊢ F ∈ S LMHom T ∧ U ∈ X → a ∈ Base Scalar ⁡ T ↔ a ∈ Base Scalar ⁡ S
27 26 biimpa ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T → a ∈ Base Scalar ⁡ S
28 27 adantrr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → a ∈ Base Scalar ⁡ S
29 17 sselda ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ c ∈ U → c ∈ Base S
30 29 adantrl ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → c ∈ Base S
31 eqid ⊢ Base Scalar ⁡ S = Base Scalar ⁡ S
32 eqid ⊢ ⋅ S = ⋅ S
33 eqid ⊢ ⋅ T = ⋅ T
34 21 31 10 32 33 lmhmlin ⊢ F ∈ S LMHom T ∧ a ∈ Base Scalar ⁡ S ∧ c ∈ Base S → F ⁡ a ⋅ S c = a ⋅ T F ⁡ c
35 20 28 30 34 syl3anc ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → F ⁡ a ⋅ S c = a ⋅ T F ⁡ c
36 20 12 14 3syl ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → F Fn Base S
37 simplr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → U ∈ X
38 37 16 syl ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → U ⊆ Base S
39 4 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X → S ∈ LMod
40 39 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → S ∈ LMod
41 simprr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → c ∈ U
42 21 32 31 1 lssvscl ⊢ S ∈ LMod ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ S ∧ c ∈ U → a ⋅ S c ∈ U
43 40 37 28 41 42 syl22anc ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → a ⋅ S c ∈ U
44 fnfvima ⊢ F Fn Base S ∧ U ⊆ Base S ∧ a ⋅ S c ∈ U → F ⁡ a ⋅ S c ∈ F U
45 36 38 43 44 syl3anc ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → F ⁡ a ⋅ S c ∈ F U
46 35 45 eqeltrrd ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → a ⋅ T F ⁡ c ∈ F U
47 46 anassrs ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → a ⋅ T F ⁡ c ∈ F U
48 oveq2 ⊢ F ⁡ c = b → a ⋅ T F ⁡ c = a ⋅ T b
49 48 eleq1d ⊢ F ⁡ c = b → a ⋅ T F ⁡ c ∈ F U ↔ a ⋅ T b ∈ F U
50 47 49 syl5ibcom ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ c ∈ U → F ⁡ c = b → a ⋅ T b ∈ F U
51 50 rexlimdva ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T → ∃ c ∈ U F ⁡ c = b → a ⋅ T b ∈ F U
52 19 51 sylbid ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T → b ∈ F U → a ⋅ T b ∈ F U
53 52 impr ⊢ F ∈ S LMHom T ∧ U ∈ X ∧ a ∈ Base Scalar ⁡ T ∧ b ∈ F U → a ⋅ T b ∈ F U
54 53 ralrimivva ⊢ F ∈ S LMHom T ∧ U ∈ X → ∀ a ∈ Base Scalar ⁡ T ∀ b ∈ F U a ⋅ T b ∈ F U
55 lmhmlmod2 ⊢ F ∈ S LMHom T → T ∈ LMod
56 55 adantr ⊢ F ∈ S LMHom T ∧ U ∈ X → T ∈ LMod
57 eqid ⊢ Base Scalar ⁡ T = Base Scalar ⁡ T
58 22 57 11 33 2 islss4 ⊢ T ∈ LMod → F U ∈ Y ↔ F U ∈ SubGrp ⁡ T ∧ ∀ a ∈ Base Scalar ⁡ T ∀ b ∈ F U a ⋅ T b ∈ F U
59 56 58 syl ⊢ F ∈ S LMHom T ∧ U ∈ X → F U ∈ Y ↔ F U ∈ SubGrp ⁡ T ∧ ∀ a ∈ Base Scalar ⁡ T ∀ b ∈ F U a ⋅ T b ∈ F U
60 9 54 59 mpbir2and ⊢ F ∈ S LMHom T ∧ U ∈ X → F U ∈ Y