Metamath Proof Explorer

Theorem pwssub

Description: Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015)

Ref Expression
Hypotheses pwsgrp.y 
|- Y = ( R ^s I )
pwsinvg.b 
|- B = ( Base ` Y )
pwssub.m 
|- M = ( -g ` R )
pwssub.n 
|- .- = ( -g ` Y )
Assertion pwssub 
|- ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )

Proof

Step Hyp Ref Expression
1 pwsgrp.y 
 |-  Y = ( R ^s I )
2 pwsinvg.b 
 |-  B = ( Base ` Y )
3 pwssub.m 
 |-  M = ( -g ` R )
4 pwssub.n 
 |-  .- = ( -g ` Y )
5 simplr 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> I e. V )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 simpll 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> R e. Grp )
8 simprl 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> F e. B )
9 1 6 2 7 5 8 pwselbas 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> F : I --> ( Base ` R ) )
10 9 ffvelrnda 
 |-  ( ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) /\ x e. I ) -> ( F ` x ) e. ( Base ` R ) )
11 fvexd 
 |-  ( ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) /\ x e. I ) -> ( ( invg ` R ) ` ( G ` x ) ) e. _V )
12 9 feqmptd 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> F = ( x e. I |-> ( F ` x ) ) )
13 simprr 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> G e. B )
14 eqid 
 |-  ( invg ` R ) = ( invg ` R )
15 eqid 
 |-  ( invg ` Y ) = ( invg ` Y )
16 1 2 14 15 pwsinvg 
 |-  ( ( R e. Grp /\ I e. V /\ G e. B ) -> ( ( invg ` Y ) ` G ) = ( ( invg ` R ) o. G ) )
17 7 5 13 16 syl3anc 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( ( invg ` Y ) ` G ) = ( ( invg ` R ) o. G ) )
18 1 6 2 7 5 13 pwselbas 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> G : I --> ( Base ` R ) )
19 18 ffvelrnda 
 |-  ( ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) /\ x e. I ) -> ( G ` x ) e. ( Base ` R ) )
20 18 feqmptd 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> G = ( x e. I |-> ( G ` x ) ) )
21 6 14 grpinvf 
 |-  ( R e. Grp -> ( invg ` R ) : ( Base ` R ) --> ( Base ` R ) )
22 21 ad2antrr 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( invg ` R ) : ( Base ` R ) --> ( Base ` R ) )
23 22 feqmptd 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( invg ` R ) = ( y e. ( Base ` R ) |-> ( ( invg ` R ) ` y ) ) )
24 fveq2 
 |-  ( y = ( G ` x ) -> ( ( invg ` R ) ` y ) = ( ( invg ` R ) ` ( G ` x ) ) )
25 19 20 23 24 fmptco 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( ( invg ` R ) o. G ) = ( x e. I |-> ( ( invg ` R ) ` ( G ` x ) ) ) )
26 17 25 eqtrd 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( ( invg ` Y ) ` G ) = ( x e. I |-> ( ( invg ` R ) ` ( G ` x ) ) ) )
27 5 10 11 12 26 offval2 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F oF ( +g ` R ) ( ( invg ` Y ) ` G ) ) = ( x e. I |-> ( ( F ` x ) ( +g ` R ) ( ( invg ` R ) ` ( G ` x ) ) ) ) )
28 1 pwsgrp 
 |-  ( ( R e. Grp /\ I e. V ) -> Y e. Grp )
29 2 15 grpinvcl 
 |-  ( ( Y e. Grp /\ G e. B ) -> ( ( invg ` Y ) ` G ) e. B )
30 28 13 29 syl2an2r 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( ( invg ` Y ) ` G ) e. B )
31 eqid 
 |-  ( +g ` R ) = ( +g ` R )
32 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
33 1 2 7 5 8 30 31 32 pwsplusgval 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) = ( F oF ( +g ` R ) ( ( invg ` Y ) ` G ) ) )
34 6 31 14 3 grpsubval 
 |-  ( ( ( F ` x ) e. ( Base ` R ) /\ ( G ` x ) e. ( Base ` R ) ) -> ( ( F ` x ) M ( G ` x ) ) = ( ( F ` x ) ( +g ` R ) ( ( invg ` R ) ` ( G ` x ) ) ) )
35 10 19 34 syl2anc 
 |-  ( ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) /\ x e. I ) -> ( ( F ` x ) M ( G ` x ) ) = ( ( F ` x ) ( +g ` R ) ( ( invg ` R ) ` ( G ` x ) ) ) )
36 35 mpteq2dva 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( x e. I |-> ( ( F ` x ) M ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( +g ` R ) ( ( invg ` R ) ` ( G ` x ) ) ) ) )
37 27 33 36 3eqtr4d 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) = ( x e. I |-> ( ( F ` x ) M ( G ` x ) ) ) )
38 2 32 15 4 grpsubval 
 |-  ( ( F e. B /\ G e. B ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
39 38 adantl 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )
40 5 10 19 12 20 offval2 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F oF M G ) = ( x e. I |-> ( ( F ` x ) M ( G ` x ) ) ) )
41 37 39 40 3eqtr4d 
 |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )