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 
|- Y = ( W ^s U )
pwssplit1.z 
|- Z = ( W ^s V )
pwssplit1.b 
|- B = ( Base ` Y )
pwssplit1.c 
|- C = ( Base ` Z )
pwssplit1.f 
|- F = ( x e. B |-> ( x |` V ) )
Assertion pwssplit2 
|- ( ( W e. Grp /\ U e. X /\ V C_ U ) -> F e. ( Y GrpHom Z ) )

Proof

Step Hyp Ref Expression
1 pwssplit1.y 
 |-  Y = ( W ^s U )
2 pwssplit1.z 
 |-  Z = ( W ^s V )
3 pwssplit1.b 
 |-  B = ( Base ` Y )
4 pwssplit1.c 
 |-  C = ( Base ` Z )
5 pwssplit1.f 
 |-  F = ( x e. B |-> ( x |` V ) )
6 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
7 eqid 
 |-  ( +g ` Z ) = ( +g ` Z )
8 simp1 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> W e. Grp )
9 simp2 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> U e. X )
10 1 pwsgrp 
 |-  ( ( W e. Grp /\ U e. X ) -> Y e. Grp )
11 8 9 10 syl2anc 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> Y e. Grp )
12 simp3 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> V C_ U )
13 9 12 ssexd 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> V e. _V )
14 2 pwsgrp 
 |-  ( ( W e. Grp /\ V e. _V ) -> Z e. Grp )
15 8 13 14 syl2anc 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> Z e. Grp )
16 1 2 3 4 5 pwssplit0 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> F : B --> C )
17 offres 
 |-  ( ( a e. B /\ b e. B ) -> ( ( a oF ( +g ` W ) b ) |` V ) = ( ( a |` V ) oF ( +g ` W ) ( b |` V ) ) )
18 17 adantl 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( ( a oF ( +g ` W ) b ) |` V ) = ( ( a |` V ) oF ( +g ` W ) ( b |` V ) ) )
19 8 adantr 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> W e. Grp )
20 simpl2 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> U e. X )
21 simprl 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
22 simprr 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
23 eqid 
 |-  ( +g ` W ) = ( +g ` W )
24 1 3 19 20 21 22 23 6 pwsplusgval 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` Y ) b ) = ( a oF ( +g ` W ) b ) )
25 24 reseq1d 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( ( a ( +g ` Y ) b ) |` V ) = ( ( a oF ( +g ` W ) b ) |` V ) )
26 5 fvtresfn 
 |-  ( a e. B -> ( F ` a ) = ( a |` V ) )
27 5 fvtresfn 
 |-  ( b e. B -> ( F ` b ) = ( b |` V ) )
28 26 27 oveqan12d 
 |-  ( ( a e. B /\ b e. B ) -> ( ( F ` a ) oF ( +g ` W ) ( F ` b ) ) = ( ( a |` V ) oF ( +g ` W ) ( b |` V ) ) )
29 28 adantl 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) oF ( +g ` W ) ( F ` b ) ) = ( ( a |` V ) oF ( +g ` W ) ( b |` V ) ) )
30 18 25 29 3eqtr4d 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( ( a ( +g ` Y ) b ) |` V ) = ( ( F ` a ) oF ( +g ` W ) ( F ` b ) ) )
31 3 6 grpcl 
 |-  ( ( Y e. Grp /\ a e. B /\ b e. B ) -> ( a ( +g ` Y ) b ) e. B )
32 31 3expb 
 |-  ( ( Y e. Grp /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` Y ) b ) e. B )
33 11 32 sylan 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` Y ) b ) e. B )
34 5 fvtresfn 
 |-  ( ( a ( +g ` Y ) b ) e. B -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( a ( +g ` Y ) b ) |` V ) )
35 33 34 syl 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( a ( +g ` Y ) b ) |` V ) )
36 13 adantr 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> V e. _V )
37 16 ffvelrnda 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ a e. B ) -> ( F ` a ) e. C )
38 37 adantrr 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) e. C )
39 16 ffvelrnda 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ b e. B ) -> ( F ` b ) e. C )
40 39 adantrl 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) e. C )
41 2 4 19 36 38 40 23 7 pwsplusgval 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( ( F ` a ) ( +g ` Z ) ( F ` b ) ) = ( ( F ` a ) oF ( +g ` W ) ( F ` b ) ) )
42 30 35 41 3eqtr4d 
 |-  ( ( ( W e. Grp /\ U e. X /\ V C_ U ) /\ ( a e. B /\ b e. B ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` Z ) ( F ` b ) ) )
43 3 4 6 7 11 15 16 42 isghmd 
 |-  ( ( W e. Grp /\ U e. X /\ V C_ U ) -> F e. ( Y GrpHom Z ) )