Step | Hyp | Ref
| Expression |
1 | | lmghm 18852 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
3 | | lmhmlmod1 18854 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝑆 ∈ LMod) |
5 | | simpr 476 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝑈 ∈ 𝑋) |
6 | | lmhmima.x |
. . . . 5
⊢ 𝑋 = (LSubSp‘𝑆) |
7 | 6 | lsssubg 18778 |
. . . 4
⊢ ((𝑆 ∈ LMod ∧ 𝑈 ∈ 𝑋) → 𝑈 ∈ (SubGrp‘𝑆)) |
8 | 4, 5, 7 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝑈 ∈ (SubGrp‘𝑆)) |
9 | | ghmima 17504 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑆)) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇)) |
10 | 2, 8, 9 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇)) |
11 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑇) =
(Base‘𝑇) |
13 | 11, 12 | lmhmf 18855 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
14 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
15 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝐹 Fn (Base‘𝑆)) |
17 | 11, 6 | lssss 18758 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑋 → 𝑈 ⊆ (Base‘𝑆)) |
18 | 5, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝑈 ⊆ (Base‘𝑆)) |
19 | | fvelimab 6163 |
. . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝑈 ⊆ (Base‘𝑆)) → (𝑏 ∈ (𝐹 “ 𝑈) ↔ ∃𝑐 ∈ 𝑈 (𝐹‘𝑐) = 𝑏)) |
20 | 16, 18, 19 | syl2anc 691 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝑏 ∈ (𝐹 “ 𝑈) ↔ ∃𝑐 ∈ 𝑈 (𝐹‘𝑐) = 𝑏)) |
21 | 20 | adantr 480 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → (𝑏 ∈ (𝐹 “ 𝑈) ↔ ∃𝑐 ∈ 𝑈 (𝐹‘𝑐) = 𝑏)) |
22 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
23 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
24 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
25 | 23, 24 | lmhmsca 18851 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
27 | 26 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (Base‘(Scalar‘𝑇)) =
(Base‘(Scalar‘𝑆))) |
28 | 27 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝑎 ∈ (Base‘(Scalar‘𝑇)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑆)))) |
29 | 28 | biimpa 500 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
30 | 29 | adantrr 749 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
31 | 18 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑆)) |
32 | 31 | adantrl 748 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑐 ∈ (Base‘𝑆)) |
33 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
34 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
35 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
36 | 23, 33, 11, 34, 35 | lmhmlin 18856 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑐 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑐)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐))) |
37 | 22, 30, 32, 36 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑐)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐))) |
38 | 22, 13, 15 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝐹 Fn (Base‘𝑆)) |
39 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑈 ∈ 𝑋) |
40 | 39, 17 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑈 ⊆ (Base‘𝑆)) |
41 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑆 ∈ LMod) |
42 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → 𝑐 ∈ 𝑈) |
43 | 23, 34, 33, 6 | lssvscl 18776 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ LMod ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑐 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑆)𝑐) ∈ 𝑈) |
44 | 41, 39, 30, 42, 43 | syl22anc 1319 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑆)𝑐) ∈ 𝑈) |
45 | | fnfvima 6400 |
. . . . . . . . . 10
⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝑈 ⊆ (Base‘𝑆) ∧ (𝑎( ·𝑠
‘𝑆)𝑐) ∈ 𝑈) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑐)) ∈ (𝐹 “ 𝑈)) |
46 | 38, 40, 44, 45 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑐)) ∈ (𝐹 “ 𝑈)) |
47 | 37, 46 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑐 ∈ 𝑈)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐)) ∈ (𝐹 “ 𝑈)) |
48 | 47 | anassrs 678 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) ∧ 𝑐 ∈ 𝑈) → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐)) ∈ (𝐹 “ 𝑈)) |
49 | | oveq2 6557 |
. . . . . . . 8
⊢ ((𝐹‘𝑐) = 𝑏 → (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐)) = (𝑎( ·𝑠
‘𝑇)𝑏)) |
50 | 49 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝐹‘𝑐) = 𝑏 → ((𝑎( ·𝑠
‘𝑇)(𝐹‘𝑐)) ∈ (𝐹 “ 𝑈) ↔ (𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈))) |
51 | 48, 50 | syl5ibcom 234 |
. . . . . 6
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) ∧ 𝑐 ∈ 𝑈) → ((𝐹‘𝑐) = 𝑏 → (𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈))) |
52 | 51 | rexlimdva 3013 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → (∃𝑐 ∈ 𝑈 (𝐹‘𝑐) = 𝑏 → (𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈))) |
53 | 21, 52 | sylbid 229 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → (𝑏 ∈ (𝐹 “ 𝑈) → (𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈))) |
54 | 53 | impr 647 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ (𝐹 “ 𝑈))) → (𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈)) |
55 | 54 | ralrimivva 2954 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → ∀𝑎 ∈ (Base‘(Scalar‘𝑇))∀𝑏 ∈ (𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈)) |
56 | | lmhmlmod2 18853 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
57 | 56 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → 𝑇 ∈ LMod) |
58 | | eqid 2610 |
. . . 4
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
59 | | lmhmima.y |
. . . 4
⊢ 𝑌 = (LSubSp‘𝑇) |
60 | 24, 58, 12, 35, 59 | islss4 18783 |
. . 3
⊢ (𝑇 ∈ LMod → ((𝐹 “ 𝑈) ∈ 𝑌 ↔ ((𝐹 “ 𝑈) ∈ (SubGrp‘𝑇) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑇))∀𝑏 ∈ (𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈)))) |
61 | 57, 60 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → ((𝐹 “ 𝑈) ∈ 𝑌 ↔ ((𝐹 “ 𝑈) ∈ (SubGrp‘𝑇) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑇))∀𝑏 ∈ (𝐹 “ 𝑈)(𝑎( ·𝑠
‘𝑇)𝑏) ∈ (𝐹 “ 𝑈)))) |
62 | 10, 55, 61 | mpbir2and 959 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ 𝑋) → (𝐹 “ 𝑈) ∈ 𝑌) |