Metamath Proof Explorer

Theorem pwssplit2

Description: Splitting for structure powers, part 2: restriction is a group 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 pwssplit2 ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 GrpHom 𝑍 ) )

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 ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
7 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
8 simp1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑊 ∈ Grp )
9 simp2 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑈 ∈ 𝑋 )
10 1 pwsgrp ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ) → 𝑌 ∈ Grp )
11 8 9 10 syl2anc ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑌 ∈ Grp )
12 simp3 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 )
13 9 12 ssexd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ∈ V )
14 2 pwsgrp ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑉 ∈ V ) → 𝑍 ∈ Grp )
15 8 13 14 syl2anc ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑍 ∈ Grp )
16 1 2 3 4 5 pwssplit0 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
17 offres ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ∘f ( +g ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝑎 ↾ 𝑉 ) ∘f ( +g ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
18 17 adantl ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ∘f ( +g ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝑎 ↾ 𝑉 ) ∘f ( +g ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
19 8 adantr ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑊 ∈ Grp )
20 simpl2 ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑈 ∈ 𝑋 )
21 simprl ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
22 simprr ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
23 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
24 1 3 19 20 21 22 23 6 pwsplusgval ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = ( 𝑎 ∘f ( +g ‘ 𝑊 ) 𝑏 ) )
25 24 reseq1d ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝑎 ∘f ( +g ‘ 𝑊 ) 𝑏 ) ↾ 𝑉 ) )
26 5 fvtresfn ⊢ ( 𝑎 ∈ 𝐵 → ( 𝐹 ‘ 𝑎 ) = ( 𝑎 ↾ 𝑉 ) )
27 5 fvtresfn ⊢ ( 𝑏 ∈ 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝑏 ↾ 𝑉 ) )
28 26 27 oveqan12d ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ∘f ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑎 ↾ 𝑉 ) ∘f ( +g ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
29 28 adantl ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) ∘f ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝑎 ↾ 𝑉 ) ∘f ( +g ‘ 𝑊 ) ( 𝑏 ↾ 𝑉 ) ) )
30 18 25 29 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) = ( ( 𝐹 ‘ 𝑎 ) ∘f ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) )
31 3 6 grpcl ⊢ ( ( 𝑌 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
32 31 3expb ⊢ ( ( 𝑌 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
33 11 32 sylan ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
34 5 fvtresfn ⊢ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) )
35 33 34 syl ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ↾ 𝑉 ) )
36 13 adantr ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑉 ∈ V )
37 16 ffvelrnda ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐶 )
38 37 adantrr ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐶 )
39 16 ffvelrnda ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐶 )
40 39 adantrl ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐶 )
41 2 4 19 36 38 40 23 7 pwsplusgval ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑍 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ∘f ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑏 ) ) )
42 30 35 41 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑍 ) ( 𝐹 ‘ 𝑏 ) ) )
43 3 4 6 7 11 15 16 42 isghmd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 ∈ ( 𝑌 GrpHom 𝑍 ) )