| Step | Hyp | Ref
| Expression |
| 1 | | lmghm 21030 |
. . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
| 2 | | lmhmlmod2 21031 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
| 3 | | lmhmima.y |
. . . . 5
⊢ 𝑌 = (LSubSp‘𝑇) |
| 4 | 3 | lsssubg 20955 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
| 5 | 2, 4 | sylan 580 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
| 6 | | ghmpreima 19256 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
| 7 | 1, 5, 6 | syl2an2r 685 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
| 8 | | lmhmlmod1 21032 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
| 9 | 8 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑆 ∈ LMod) |
| 10 | | simprl 771 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
| 11 | | cnvimass 6100 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 |
| 12 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑇) =
(Base‘𝑇) |
| 14 | 12, 13 | lmhmf 21033 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
| 15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
| 16 | 11, 15 | fssdm 6755 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ⊆ (Base‘𝑆)) |
| 17 | 16 | sselda 3983 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → 𝑏 ∈ (Base‘𝑆)) |
| 18 | 17 | adantrl 716 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (Base‘𝑆)) |
| 19 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
| 20 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
| 21 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
| 22 | 12, 19, 20, 21 | lmodvscl 20876 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 23 | 9, 10, 18, 22 | syl3anc 1373 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
| 24 | | simpll 767 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
| 26 | 19, 21, 12, 20, 25 | lmhmlin 21034 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
| 27 | 24, 10, 18, 26 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
| 28 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑇 ∈ LMod) |
| 29 | | simplr 769 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑈 ∈ 𝑌) |
| 30 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
| 31 | 19, 30 | lmhmsca 21029 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
| 33 | 32 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Base‘(Scalar‘𝑇)) =
(Base‘(Scalar‘𝑆))) |
| 34 | 33 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑆)))) |
| 35 | 34 | biimpar 477 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
| 36 | 35 | adantrr 717 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
| 37 | 15 | ffund 6740 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → Fun 𝐹) |
| 38 | | simprr 773 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (◡𝐹 “ 𝑈)) |
| 39 | | fvimacnvi 7072 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → (𝐹‘𝑏) ∈ 𝑈) |
| 40 | 37, 38, 39 | syl2an2r 685 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘𝑏) ∈ 𝑈) |
| 41 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
| 42 | 30, 25, 41, 3 | lssvscl 20953 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐹‘𝑏) ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
| 43 | 28, 29, 36, 40, 42 | syl22anc 839 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
| 44 | 27, 43 | eqeltrd 2841 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈) |
| 45 | | ffn 6736 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
| 46 | | elpreima 7078 |
. . . . . 6
⊢ (𝐹 Fn (Base‘𝑆) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
| 47 | 15, 45, 46 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
| 48 | 47 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
| 49 | 23, 44, 48 | mpbir2and 713 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
| 50 | 49 | ralrimivva 3202 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
| 51 | 8 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑆 ∈ LMod) |
| 52 | | lmhmima.x |
. . . 4
⊢ 𝑋 = (LSubSp‘𝑆) |
| 53 | 19, 21, 12, 20, 52 | islss4 20960 |
. . 3
⊢ (𝑆 ∈ LMod → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
| 54 | 51, 53 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
| 55 | 7, 50, 54 | mpbir2and 713 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) |