| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lmhmlmod1 21032 | . . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | 
| 2 |  | reslmhm.r | . . . 4
⊢ 𝑅 = (𝑆 ↾s 𝑋) | 
| 3 |  | reslmhm.u | . . . 4
⊢ 𝑈 = (LSubSp‘𝑆) | 
| 4 | 2, 3 | lsslmod 20958 | . . 3
⊢ ((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ LMod) | 
| 5 | 1, 4 | sylan 580 | . 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ LMod) | 
| 6 |  | lmhmlmod2 21031 | . . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | 
| 7 | 6 | adantr 480 | . 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑇 ∈ LMod) | 
| 8 |  | lmghm 21030 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | 
| 9 | 3 | lsssubg 20955 | . . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (SubGrp‘𝑆)) | 
| 10 | 1, 9 | sylan 580 | . . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (SubGrp‘𝑆)) | 
| 11 | 2 | resghm 19250 | . . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇)) | 
| 12 | 8, 10, 11 | syl2an2r 685 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇)) | 
| 13 |  | eqid 2737 | . . . . 5
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) | 
| 14 |  | eqid 2737 | . . . . 5
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) | 
| 15 | 13, 14 | lmhmsca 21029 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) | 
| 16 | 2, 13 | resssca 17387 | . . . 4
⊢ (𝑋 ∈ 𝑈 → (Scalar‘𝑆) = (Scalar‘𝑅)) | 
| 17 | 15, 16 | sylan9eq 2797 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Scalar‘𝑇) = (Scalar‘𝑅)) | 
| 18 |  | simpll 767 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | 
| 19 |  | simprl 771 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) | 
| 20 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 21 | 20, 3 | lssss 20934 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝑈 → 𝑋 ⊆ (Base‘𝑆)) | 
| 22 | 21 | adantl 481 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 ⊆ (Base‘𝑆)) | 
| 23 | 22 | adantr 480 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑋 ⊆ (Base‘𝑆)) | 
| 24 | 2, 20 | ressbas2 17283 | . . . . . . . . . . . 12
⊢ (𝑋 ⊆ (Base‘𝑆) → 𝑋 = (Base‘𝑅)) | 
| 25 | 22, 24 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑋 = (Base‘𝑅)) | 
| 26 | 25 | eleq2d 2827 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝑏 ∈ 𝑋 ↔ 𝑏 ∈ (Base‘𝑅))) | 
| 27 | 26 | biimpar 477 | . . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑏 ∈ 𝑋) | 
| 28 | 27 | adantrl 716 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ 𝑋) | 
| 29 | 23, 28 | sseldd 3984 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ (Base‘𝑆)) | 
| 30 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) | 
| 31 |  | eqid 2737 | . . . . . . . 8
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) | 
| 32 |  | eqid 2737 | . . . . . . . 8
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) | 
| 33 | 13, 30, 20, 31, 32 | lmhmlin 21034 | . . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑆)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) | 
| 34 | 18, 19, 29, 33 | syl3anc 1373 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) | 
| 35 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → 𝑆 ∈ LMod) | 
| 36 | 35 | adantr 480 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑆 ∈ LMod) | 
| 37 |  | simplr 769 | . . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑋 ∈ 𝑈) | 
| 38 | 13, 31, 30, 3 | lssvscl 20953 | . . . . . . . 8
⊢ (((𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ 𝑋)) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ 𝑋) | 
| 39 | 36, 37, 19, 28, 38 | syl22anc 839 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎( ·𝑠
‘𝑆)𝑏) ∈ 𝑋) | 
| 40 | 39 | fvresd 6926 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝐹‘(𝑎( ·𝑠
‘𝑆)𝑏))) | 
| 41 |  | fvres 6925 | . . . . . . . 8
⊢ (𝑏 ∈ 𝑋 → ((𝐹 ↾ 𝑋)‘𝑏) = (𝐹‘𝑏)) | 
| 42 | 41 | oveq2d 7447 | . . . . . . 7
⊢ (𝑏 ∈ 𝑋 → (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) | 
| 43 | 28, 42 | syl 17 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) = (𝑎( ·𝑠
‘𝑇)(𝐹‘𝑏))) | 
| 44 | 34, 40, 43 | 3eqtr4d 2787 | . . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) | 
| 45 | 44 | ralrimivva 3202 | . . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) | 
| 46 | 16 | adantl 481 | . . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Scalar‘𝑆) = (Scalar‘𝑅)) | 
| 47 | 46 | fveq2d 6910 | . . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (Base‘(Scalar‘𝑆)) =
(Base‘(Scalar‘𝑅))) | 
| 48 | 2, 31 | ressvsca 17388 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑈 → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑅)) | 
| 49 | 48 | adantl 481 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑅)) | 
| 50 | 49 | oveqd 7448 | . . . . . . 7
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝑎( ·𝑠
‘𝑆)𝑏) = (𝑎( ·𝑠
‘𝑅)𝑏)) | 
| 51 | 50 | fveqeq2d 6914 | . . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) | 
| 52 | 51 | ralbidv 3178 | . . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) | 
| 53 | 47, 52 | raleqbidv 3346 | . . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (∀𝑎 ∈ (Base‘(Scalar‘𝑆))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑆)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)) ↔ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) | 
| 54 | 45, 53 | mpbid 232 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))) | 
| 55 | 12, 17, 54 | 3jca 1129 | . 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → ((𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑅) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏)))) | 
| 56 |  | eqid 2737 | . . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) | 
| 57 |  | eqid 2737 | . . 3
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) | 
| 58 |  | eqid 2737 | . . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 59 |  | eqid 2737 | . . 3
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) | 
| 60 | 56, 14, 57, 58, 59, 32 | islmhm 21026 | . 2
⊢ ((𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇) ↔ ((𝑅 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ ((𝐹 ↾ 𝑋) ∈ (𝑅 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑅) ∧ ∀𝑎 ∈ (Base‘(Scalar‘𝑅))∀𝑏 ∈ (Base‘𝑅)((𝐹 ↾ 𝑋)‘(𝑎( ·𝑠
‘𝑅)𝑏)) = (𝑎( ·𝑠
‘𝑇)((𝐹 ↾ 𝑋)‘𝑏))))) | 
| 61 | 5, 7, 55, 60 | syl21anbrc 1345 | 1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑋 ∈ 𝑈) → (𝐹 ↾ 𝑋) ∈ (𝑅 LMHom 𝑇)) |