Step | Hyp | Ref
| Expression |
1 | | lmghm 18852 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
3 | | lmhmlmod2 18853 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
4 | | lmhmima.y |
. . . . 5
⊢ 𝑌 = (LSubSp‘𝑇) |
5 | 4 | lsssubg 18778 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
6 | 3, 5 | sylan 487 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
7 | | ghmpreima 17505 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
8 | 2, 6, 7 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
9 | | lmhmlmod1 18854 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
10 | 9 | ad2antrr 758 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑆 ∈ LMod) |
11 | | simprl 790 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
12 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 |
13 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑇) =
(Base‘𝑇) |
15 | 13, 14 | lmhmf 18855 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
17 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → dom 𝐹 = (Base‘𝑆)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → dom 𝐹 = (Base‘𝑆)) |
19 | 12, 18 | syl5sseq 3616 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ⊆ (Base‘𝑆)) |
20 | 19 | sselda 3568 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → 𝑏 ∈ (Base‘𝑆)) |
21 | 20 | adantrl 748 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (Base‘𝑆)) |
22 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
23 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
24 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
25 | 13, 22, 23, 24 | lmodvscl 18703 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
26 | 10, 11, 21, 25 | syl3anc 1318 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
27 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
28 | | eqid 2610 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
29 | 22, 24, 13, 23, 28 | lmhmlin 18856 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
30 | 27, 11, 21, 29 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
31 | 3 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑇 ∈ LMod) |
32 | | simplr 788 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑈 ∈ 𝑌) |
33 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
34 | 22, 33 | lmhmsca 18851 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
35 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
36 | 35 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Base‘(Scalar‘𝑇)) =
(Base‘(Scalar‘𝑆))) |
37 | 36 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑆)))) |
38 | 37 | biimpar 501 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
39 | 38 | adantrr 749 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
40 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → Fun 𝐹) |
41 | 16, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → Fun 𝐹) |
42 | 41 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → Fun 𝐹) |
43 | | simprr 792 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (◡𝐹 “ 𝑈)) |
44 | | fvimacnvi 6239 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → (𝐹‘𝑏) ∈ 𝑈) |
45 | 42, 43, 44 | syl2anc 691 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘𝑏) ∈ 𝑈) |
46 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
47 | 33, 28, 46, 4 | lssvscl 18776 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐹‘𝑏) ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
48 | 31, 32, 39, 45, 47 | syl22anc 1319 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
49 | 30, 48 | eqeltrd 2688 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈) |
50 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
51 | | elpreima 6245 |
. . . . . 6
⊢ (𝐹 Fn (Base‘𝑆) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
52 | 16, 50, 51 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
53 | 52 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
54 | 26, 49, 53 | mpbir2and 959 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
55 | 54 | ralrimivva 2954 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
56 | 9 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑆 ∈ LMod) |
57 | | lmhmima.x |
. . . 4
⊢ 𝑋 = (LSubSp‘𝑆) |
58 | 22, 24, 13, 23, 57 | islss4 18783 |
. . 3
⊢ (𝑆 ∈ LMod → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
59 | 56, 58 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
60 | 8, 55, 59 | mpbir2and 959 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) |