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 𝑍 ) )