# 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) )`
` |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F oF M G ) = ( x e. I |-> ( ( F ` x ) M ( G ` x ) ) ) )`
` |-  ( ( ( R e. Grp /\ I e. V ) /\ ( F e. B /\ G e. B ) ) -> ( F .- G ) = ( F oF M G ) )`