Step | Hyp | Ref
| Expression |
1 | | lmhmlmod1 19033 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
2 | | reslmhm.r |
. . . . 5
⊢ 𝑅 = (𝑆 ↾s 𝑋) |
3 | | reslmhm.u |
. . . . 5
⊢ 𝑈 = (LSubSp‘𝑆) |
4 | 2, 3 | lsslmod 18960 |
. . . 4
⊢ ((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ LMod) |
5 | 1, 4 | sylan 488 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ LMod) |
6 | | lmhmlmod2 19032 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
7 | 6 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑇 ∈ LMod) |
8 | 5, 7 | jca 554 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝑅 ∈ LMod ∧ 𝑇 ∈ LMod)) |
9 | | lmghm 19031 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
10 | 9 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
11 | 3 | lsssubg 18957 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (SubGrp‘𝑆)) |
12 | 1, 11 | sylan 488 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (SubGrp‘𝑆)) |
13 | 2 | resghm 17676 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇)) |
14 | 10, 12, 13 | syl2anc 693 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇)) |
15 | | eqid 2622 |
. . . . 5
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
16 | | eqid 2622 |
. . . . 5
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
17 | 15, 16 | lmhmsca 19030 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
18 | 2, 15 | resssca 16031 |
. . . 4
⊢ (𝑋 ∈ 𝑈 → (Scalar‘𝑆) = (Scalar‘𝑅)) |
19 | 17, 18 | sylan9eq 2676 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Scalar‘𝑇) = (Scalar‘𝑅)) |
20 | | simpll 790 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
21 | | simprl 794 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
22 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) |
23 | 22, 3 | lssss 18937 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑈 → 𝑋 ⊆ (Base‘𝑆)) |
24 | 23 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 ⊆ (Base‘𝑆)) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑋 ⊆ (Base‘𝑆)) |
26 | 2, 22 | ressbas2 15931 |
. . . . . . . . . . . 12
⊢ (𝑋 ⊆ (Base‘𝑆) → 𝑋 = (Base‘𝑅)) |
27 | 24, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 = (Base‘𝑅)) |
28 | 27 | eleq2d 2687 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝑏 ∈ 𝑋 ↔ 𝑏 ∈ (Base‘𝑅))) |
29 | 28 | biimpar 502 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑏 ∈ 𝑋) |
30 | 29 | adantrl 752 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ 𝑋) |
31 | 25, 30 | sseldd 3604 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ (Base‘𝑆)) |
32 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
33 | | eqid 2622 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
34 | | eqid 2622 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
35 | 15, 32, 22, 33, 34 | lmhmlin 19035 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
36 | 20, 21, 31, 35 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
37 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑆 ∈ LMod) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑆 ∈ LMod) |
39 | | simplr 792 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑋 ∈ 𝑈) |
40 | 15, 33, 32, 3 | lssvscl 18955 |
. . . . . . . 8
⊢ (((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ 𝑋)) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ 𝑋) |
41 | 38, 39, 21, 30, 40 | syl22anc 1327 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ 𝑋) |
42 | | fvres 6207 |
. . . . . . 7
⊢ ((𝑎(
·𝑠 ‘𝑆)𝑏) ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏))) |
43 | 41, 42 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏))) |
44 | | fvres 6207 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑏) = (𝐹‘𝑏)) |
45 | 44 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑏 ∈ 𝑋 → (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
46 | 30, 45 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) |
47 | 36, 43, 46 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) |
48 | 47 | ralrimivva 2971 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) |
49 | 18 | adantl 482 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Scalar‘𝑆) = (Scalar‘𝑅)) |
50 | 49 | fveq2d 6195 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Base‘(Scalar‘𝑆)) =
(Base‘(Scalar‘𝑅))) |
51 | 2, 33 | ressvsca 16032 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑈 → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑅)) |
52 | 51 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑅)) |
53 | 52 | oveqd 6667 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝑎( ·𝑠
‘𝑆)𝑏) = (𝑎( ·𝑠
‘𝑅)𝑏)) |
54 | 53 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏))) |
55 | 54 | eqeq1d 2624 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) |
56 | 55 | ralbidv 2986 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) |
57 | 50, 56 | raleqbidv 3152 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) |
58 | 48, 57 | mpbid 222 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) |
59 | 14, 19, 58 | 3jca 1242 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ((𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑅) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) |
60 | | eqid 2622 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
61 | | eqid 2622 |
. . 3
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
62 | | eqid 2622 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
63 | | eqid 2622 |
. . 3
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
64 | 60, 16, 61, 62, 63, 34 | islmhm 19027 |
. 2
⊢ ((𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇) ↔ ((𝑅 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ ((𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑅) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))))) |
65 | 8, 59, 64 | sylanbrc 698 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇)) |