Step | Hyp | Ref
| Expression |
1 | | lmghm 19390 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
2 | 1 | adantr 474 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
3 | | lmhmlmod2 19391 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
4 | | lmhmima.y |
. . . . 5
⊢ 𝑌 = (LSubSp‘𝑇) |
5 | 4 | lsssubg 19316 |
. . . 4
⊢ ((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
6 | 3, 5 | sylan 577 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑈 ∈ (SubGrp‘𝑇)) |
7 | | ghmpreima 18033 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
8 | 2, 6, 7 | syl2anc 581 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆)) |
9 | | lmhmlmod1 19392 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
10 | 9 | ad2antrr 719 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑆 ∈ LMod) |
11 | | simprl 789 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
12 | | cnvimass 5726 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 |
13 | | eqid 2825 |
. . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) |
14 | | eqid 2825 |
. . . . . . . . . 10
⊢
(Base‘𝑇) =
(Base‘𝑇) |
15 | 13, 14 | lmhmf 19393 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
16 | 15 | adantr 474 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
17 | 12, 16 | fssdm 6294 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ⊆ (Base‘𝑆)) |
18 | 17 | sselda 3827 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → 𝑏 ∈ (Base‘𝑆)) |
19 | 18 | adantrl 709 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (Base‘𝑆)) |
20 | | eqid 2825 |
. . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
21 | | eqid 2825 |
. . . . . 6
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
22 | | eqid 2825 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
23 | 13, 20, 21, 22 | lmodvscl 19236 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
24 | 10, 11, 19, 23 | syl3anc 1496 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆)) |
25 | | simpll 785 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
26 | | eqid 2825 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
27 | 20, 22, 13, 21, 26 | lmhmlin 19394 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
28 | 25, 11, 19, 27 | syl3anc 1496 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
29 | 3 | ad2antrr 719 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑇 ∈ LMod) |
30 | | simplr 787 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑈 ∈ 𝑌) |
31 | | eqid 2825 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
32 | 20, 31 | lmhmsca 19389 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
33 | 32 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
34 | 33 | fveq2d 6437 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (Base‘(Scalar‘𝑇)) =
(Base‘(Scalar‘𝑆))) |
35 | 34 | eleq2d 2892 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑆)))) |
36 | 35 | biimpar 471 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
37 | 36 | adantrr 710 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑎 ∈ (Base‘(Scalar‘𝑇))) |
38 | 16 | ffund 6282 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → Fun 𝐹) |
39 | 38 | adantr 474 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → Fun 𝐹) |
40 | | simprr 791 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → 𝑏 ∈ (◡𝐹 “ 𝑈)) |
41 | | fvimacnvi 6580 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑏 ∈ (◡𝐹 “ 𝑈)) → (𝐹‘𝑏) ∈ 𝑈) |
42 | 39, 40, 41 | syl2anc 581 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘𝑏) ∈ 𝑈) |
43 | | eqid 2825 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
44 | 31, 26, 43, 4 | lssvscl 19314 |
. . . . . 6
⊢ (((𝑇 ∈ LMod ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ (𝐹‘𝑏) ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
45 | 29, 30, 37, 42, 44 | syl22anc 874 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏)) ∈ 𝑈) |
46 | 28, 45 | eqeltrd 2906 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈) |
47 | | ffn 6278 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
48 | | elpreima 6586 |
. . . . . 6
⊢ (𝐹 Fn (Base‘𝑆) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
49 | 16, 47, 48 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
50 | 49 | adantr 474 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈) ↔ ((𝑎( ·𝑠
‘𝑆)𝑏) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) ∈ 𝑈))) |
51 | 24, 46, 50 | mpbir2and 706 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (◡𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
52 | 51 | ralrimivva 3180 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)) |
53 | 9 | adantr 474 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → 𝑆 ∈ LMod) |
54 | | lmhmima.x |
. . . 4
⊢ 𝑋 = (LSubSp‘𝑆) |
55 | 20, 22, 13, 21, 54 | islss4 19321 |
. . 3
⊢ (𝑆 ∈ LMod → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
56 | 53, 55 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → ((◡𝐹 “ 𝑈) ∈ 𝑋 ↔ ((◡𝐹 “ 𝑈) ∈ (SubGrp‘𝑆) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (◡𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑆)𝑏) ∈ (◡𝐹 “ 𝑈)))) |
57 | 8, 52, 56 | mpbir2and 706 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑌) → (◡𝐹 “ 𝑈) ∈ 𝑋) |