| Step | Hyp | Ref
| Expression |
| 1 | | pwssplit1.b |
. 2
⊢ 𝐵 = (Base‘𝑌) |
| 2 | | eqid 2737 |
. 2
⊢ (
·𝑠 ‘𝑌) = ( ·𝑠
‘𝑌) |
| 3 | | eqid 2737 |
. 2
⊢ (
·𝑠 ‘𝑍) = ( ·𝑠
‘𝑍) |
| 4 | | eqid 2737 |
. 2
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
| 5 | | eqid 2737 |
. 2
⊢
(Scalar‘𝑍) =
(Scalar‘𝑍) |
| 6 | | eqid 2737 |
. 2
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
| 7 | | simp1 1137 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑊 ∈ LMod) |
| 8 | | simp2 1138 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑈 ∈ 𝑋) |
| 9 | | pwssplit1.y |
. . . 4
⊢ 𝑌 = (𝑊 ↑s 𝑈) |
| 10 | 9 | pwslmod 20968 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋) → 𝑌 ∈ LMod) |
| 11 | 7, 8, 10 | syl2anc 584 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑌 ∈ LMod) |
| 12 | | simp3 1139 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑉 ⊆ 𝑈) |
| 13 | 8, 12 | ssexd 5324 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑉 ∈ V) |
| 14 | | pwssplit1.z |
. . . 4
⊢ 𝑍 = (𝑊 ↑s 𝑉) |
| 15 | 14 | pwslmod 20968 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ∈ V) → 𝑍 ∈ LMod) |
| 16 | 7, 13, 15 | syl2anc 584 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝑍 ∈ LMod) |
| 17 | | eqid 2737 |
. . . . 5
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 18 | 14, 17 | pwssca 17541 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑉 ∈ V) →
(Scalar‘𝑊) =
(Scalar‘𝑍)) |
| 19 | 7, 13, 18 | syl2anc 584 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (Scalar‘𝑊) = (Scalar‘𝑍)) |
| 20 | 9, 17 | pwssca 17541 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋) → (Scalar‘𝑊) = (Scalar‘𝑌)) |
| 21 | 7, 8, 20 | syl2anc 584 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (Scalar‘𝑊) = (Scalar‘𝑌)) |
| 22 | 19, 21 | eqtr3d 2779 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (Scalar‘𝑍) = (Scalar‘𝑌)) |
| 23 | | lmodgrp 20865 |
. . 3
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 24 | | pwssplit1.c |
. . . 4
⊢ 𝐶 = (Base‘𝑍) |
| 25 | | pwssplit1.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 ↾ 𝑉)) |
| 26 | 9, 14, 1, 24, 25 | pwssplit2 21059 |
. . 3
⊢ ((𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 GrpHom 𝑍)) |
| 27 | 23, 26 | syl3an1 1164 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 GrpHom 𝑍)) |
| 28 | | snex 5436 |
. . . . . . . 8
⊢ {𝑎} ∈ V |
| 29 | | xpexg 7770 |
. . . . . . . 8
⊢ ((𝑈 ∈ 𝑋 ∧ {𝑎} ∈ V) → (𝑈 × {𝑎}) ∈ V) |
| 30 | 8, 28, 29 | sylancl 586 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (𝑈 × {𝑎}) ∈ V) |
| 31 | | vex 3484 |
. . . . . . 7
⊢ 𝑏 ∈ V |
| 32 | | offres 8008 |
. . . . . . 7
⊢ (((𝑈 × {𝑎}) ∈ V ∧ 𝑏 ∈ V) → (((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏) ↾ 𝑉) = (((𝑈 × {𝑎}) ↾ 𝑉) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 33 | 30, 31, 32 | sylancl 586 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏) ↾ 𝑉) = (((𝑈 × {𝑎}) ↾ 𝑉) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏) ↾ 𝑉) = (((𝑈 × {𝑎}) ↾ 𝑉) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 35 | | xpssres 6036 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝑈 → ((𝑈 × {𝑎}) ↾ 𝑉) = (𝑉 × {𝑎})) |
| 36 | 35 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → ((𝑈 × {𝑎}) ↾ 𝑉) = (𝑉 × {𝑎})) |
| 37 | 36 | adantr 480 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → ((𝑈 × {𝑎}) ↾ 𝑉) = (𝑉 × {𝑎})) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (((𝑈 × {𝑎}) ↾ 𝑉) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉)) = ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 39 | 34, 38 | eqtrd 2777 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏) ↾ 𝑉) = ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 40 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 41 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 42 | | simpl1 1192 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → 𝑊 ∈ LMod) |
| 43 | | simpl2 1193 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → 𝑈 ∈ 𝑋) |
| 44 | 21 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑌))) |
| 45 | 44 | eleq2d 2827 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → (𝑎 ∈ (Base‘(Scalar‘𝑊)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑌)))) |
| 46 | 45 | biimpar 477 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑌))) → 𝑎 ∈ (Base‘(Scalar‘𝑊))) |
| 47 | 46 | adantrr 717 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ (Base‘(Scalar‘𝑊))) |
| 48 | | simprr 773 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
| 49 | 9, 1, 40, 2, 17, 41, 42, 43, 47, 48 | pwsvscafval 17539 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝑎( ·𝑠
‘𝑌)𝑏) = ((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏)) |
| 50 | 49 | reseq1d 5996 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → ((𝑎( ·𝑠
‘𝑌)𝑏) ↾ 𝑉) = (((𝑈 × {𝑎}) ∘f (
·𝑠 ‘𝑊)𝑏) ↾ 𝑉)) |
| 51 | 25 | fvtresfn 7018 |
. . . . . 6
⊢ (𝑏 ∈ 𝐵 → (𝐹‘𝑏) = (𝑏 ↾ 𝑉)) |
| 52 | 51 | ad2antll 729 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) = (𝑏 ↾ 𝑉)) |
| 53 | 52 | oveq2d 7447 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝐹‘𝑏)) = ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝑏 ↾ 𝑉))) |
| 54 | 39, 50, 53 | 3eqtr4d 2787 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → ((𝑎( ·𝑠
‘𝑌)𝑏) ↾ 𝑉) = ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝐹‘𝑏))) |
| 55 | 1, 4, 2, 6 | lmodvscl 20876 |
. . . . . 6
⊢ ((𝑌 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ 𝐵) |
| 56 | 55 | 3expb 1121 |
. . . . 5
⊢ ((𝑌 ∈ LMod ∧ (𝑎 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ 𝐵) |
| 57 | 11, 56 | sylan 580 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝑎( ·𝑠
‘𝑌)𝑏) ∈ 𝐵) |
| 58 | 25 | fvtresfn 7018 |
. . . 4
⊢ ((𝑎(
·𝑠 ‘𝑌)𝑏) ∈ 𝐵 → (𝐹‘(𝑎( ·𝑠
‘𝑌)𝑏)) = ((𝑎( ·𝑠
‘𝑌)𝑏) ↾ 𝑉)) |
| 59 | 57, 58 | syl 17 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎( ·𝑠
‘𝑌)𝑏)) = ((𝑎( ·𝑠
‘𝑌)𝑏) ↾ 𝑉)) |
| 60 | 13 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → 𝑉 ∈ V) |
| 61 | 9, 14, 1, 24, 25 | pwssplit0 21057 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹:𝐵⟶𝐶) |
| 62 | 61 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ 𝑏 ∈ 𝐵) → (𝐹‘𝑏) ∈ 𝐶) |
| 63 | 62 | adantrl 716 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) ∈ 𝐶) |
| 64 | 14, 24, 40, 3, 17, 41, 42, 60, 47, 63 | pwsvscafval 17539 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝑎( ·𝑠
‘𝑍)(𝐹‘𝑏)) = ((𝑉 × {𝑎}) ∘f (
·𝑠 ‘𝑊)(𝐹‘𝑏))) |
| 65 | 54, 59, 64 | 3eqtr4d 2787 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑏 ∈ 𝐵)) → (𝐹‘(𝑎( ·𝑠
‘𝑌)𝑏)) = (𝑎( ·𝑠
‘𝑍)(𝐹‘𝑏))) |
| 66 | 1, 2, 3, 4, 5, 6, 11, 16, 22, 27, 65 | islmhmd 21038 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈) → 𝐹 ∈ (𝑌 LMHom 𝑍)) |