Metamath Proof Explorer

Theorem pwssplit3

Description: Splitting for structure powers, part 3: restriction is a module homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwssplit1.y ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
Assertion pwssplit3 ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 LMHom 𝑍 ) )

Proof

Step Hyp Ref Expression
1 pwssplit1.y ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
2 pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
3 pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
5 pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
6 eqid ⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
7 eqid ⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 )
8 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
9 eqid ⊢ ( Scalar ‘ 𝑍 ) = ( Scalar ‘ 𝑍 )
10 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
11 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑊 ∈ LMod )
12 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑈 ∈ 𝑋 )
13 1 pwslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ) → 𝑌 ∈ LMod )
14 11 12 13 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑌 ∈ LMod )
15 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 )
16 12 15 ssexd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ∈ V )
17 2 pwslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ∈ V ) → 𝑍 ∈ LMod )
18 11 16 17 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑍 ∈ LMod )
19 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20 2 19 pwssca ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑉 ∈ V ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑍 ) )
21 11 16 20 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑍 ) )
22 1 19 pwssca ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑌 ) )
23 11 12 22 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑌 ) )
24 21 23 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( Scalar ‘ 𝑍 ) = ( Scalar ‘ 𝑌 ) )
25 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
26 1 2 3 4 5 pwssplit2 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 GrpHom 𝑍 ) )
27 25 26 syl3an1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 GrpHom 𝑍 ) )
28 snex ⊢ { 𝑎 } ∈ V
29 xpexg ⊢ ( ( 𝑈 ∈ 𝑋 ∧ { 𝑎 } ∈ V ) → ( 𝑈 × { 𝑎 } ) ∈ V )
30 12 28 29 sylancl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑈 × { 𝑎 } ) ∈ V )
31 vex ⊢ 𝑏 ∈ V
32 offres ⊢ ( ( ( 𝑈 × { 𝑎 } ) ∈ V ∧ 𝑏 ∈ V ) → ( ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
33 30 31 32 sylancl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
34 33 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
35 xpssres ⊢ ( 𝑉 ⊆ 𝑈 → ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) = ( 𝑉 × { 𝑎 } ) )
36 35 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) = ( 𝑉 × { 𝑎 } ) )
37 36 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) = ( 𝑉 × { 𝑎 } ) )
38 37 oveq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑈 × { 𝑎 } ) ↾ 𝑉 ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) = ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
39 34 38 eqtrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
40 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
41 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
42 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑊 ∈ LMod )
43 simpl2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑈 ∈ 𝑋 )
44 23 fveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
45 44 eleq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) )
46 45 biimpar ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
47 46 adantrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
48 simprr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
49 1 3 40 6 19 41 42 43 47 48 pwsvscafval ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) = ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) )
50 49 reseq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) = ( ( ( 𝑈 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) )
51 5 fvtresfn ⊢ ( 𝑏 ∈ 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝑏 ↾ 𝑉 ) )
52 51 ad2antll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝑏 ↾ 𝑉 ) )
53 52 oveq2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
54 39 50 53 3eqtr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) )
55 3 8 6 10 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
56 55 3expb ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
57 14 56 sylan ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
58 5 fvtresfn ⊢ ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) )
59 57 58 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) )
60 16 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → 𝑉 ∈ V )
61 1 2 3 4 5 pwssplit0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
62 61 ffvelrnda ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐶 )
63 62 adantrl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐶 )
64 2 4 40 7 19 41 42 60 47 63 pwsvscafval ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑍 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑉 × { 𝑎 } ) ∘f ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) )
65 54 59 64 3eqtr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑍 ) ( 𝐹 ‘ 𝑏 ) ) )
66 3 6 7 8 9 10 14 18 24 27 65 islmhmd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 LMHom 𝑍 ) )