# 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}{↑}_{𝑠}{I}$
pwsinvg.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
pwssub.m ${⊢}{M}={-}_{{R}}$
pwssub.n
Assertion pwssub

### Proof

Step Hyp Ref Expression
1 pwsgrp.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsinvg.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 pwssub.m ${⊢}{M}={-}_{{R}}$
4 pwssub.n
5 simplr ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {I}\in {V}$
6 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
7 simpll ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {R}\in \mathrm{Grp}$
8 simprl ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}\in {B}$
9 1 6 2 7 5 8 pwselbas ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}:{I}⟶{\mathrm{Base}}_{{R}}$
10 9 ffvelrnda ${⊢}\left(\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {F}\left({x}\right)\in {\mathrm{Base}}_{{R}}$
11 fvexd ${⊢}\left(\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)\in \mathrm{V}$
12 9 feqmptd ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}=\left({x}\in {I}⟼{F}\left({x}\right)\right)$
13 simprr ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {G}\in {B}$
14 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
15 eqid ${⊢}{inv}_{g}\left({Y}\right)={inv}_{g}\left({Y}\right)$
16 1 2 14 15 pwsinvg ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {G}\in {B}\right)\to {inv}_{g}\left({Y}\right)\left({G}\right)={inv}_{g}\left({R}\right)\circ {G}$
17 7 5 13 16 syl3anc ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({Y}\right)\left({G}\right)={inv}_{g}\left({R}\right)\circ {G}$
18 1 6 2 7 5 13 pwselbas ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {G}:{I}⟶{\mathrm{Base}}_{{R}}$
19 18 ffvelrnda ${⊢}\left(\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {G}\left({x}\right)\in {\mathrm{Base}}_{{R}}$
20 18 feqmptd ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {G}=\left({x}\in {I}⟼{G}\left({x}\right)\right)$
21 6 14 grpinvf ${⊢}{R}\in \mathrm{Grp}\to {inv}_{g}\left({R}\right):{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
22 21 ad2antrr ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({R}\right):{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
23 22 feqmptd ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({R}\right)=\left({y}\in {\mathrm{Base}}_{{R}}⟼{inv}_{g}\left({R}\right)\left({y}\right)\right)$
24 fveq2 ${⊢}{y}={G}\left({x}\right)\to {inv}_{g}\left({R}\right)\left({y}\right)={inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)$
25 19 20 23 24 fmptco ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({R}\right)\circ {G}=\left({x}\in {I}⟼{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)\right)$
26 17 25 eqtrd ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({Y}\right)\left({G}\right)=\left({x}\in {I}⟼{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)\right)$
27 5 10 11 12 26 offval2 ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}{{+}_{{R}}}_{f}{inv}_{g}\left({Y}\right)\left({G}\right)=\left({x}\in {I}⟼{F}\left({x}\right){+}_{{R}}{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)\right)$
28 1 pwsgrp ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {Y}\in \mathrm{Grp}$
29 2 15 grpinvcl ${⊢}\left({Y}\in \mathrm{Grp}\wedge {G}\in {B}\right)\to {inv}_{g}\left({Y}\right)\left({G}\right)\in {B}$
30 28 13 29 syl2an2r ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {inv}_{g}\left({Y}\right)\left({G}\right)\in {B}$
31 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
32 eqid ${⊢}{+}_{{Y}}={+}_{{Y}}$
33 1 2 7 5 8 30 31 32 pwsplusgval ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}{+}_{{Y}}{inv}_{g}\left({Y}\right)\left({G}\right)={F}{{+}_{{R}}}_{f}{inv}_{g}\left({Y}\right)\left({G}\right)$
34 6 31 14 3 grpsubval ${⊢}\left({F}\left({x}\right)\in {\mathrm{Base}}_{{R}}\wedge {G}\left({x}\right)\in {\mathrm{Base}}_{{R}}\right)\to {F}\left({x}\right){M}{G}\left({x}\right)={F}\left({x}\right){+}_{{R}}{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)$
35 10 19 34 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {x}\in {I}\right)\to {F}\left({x}\right){M}{G}\left({x}\right)={F}\left({x}\right){+}_{{R}}{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)$
36 35 mpteq2dva ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to \left({x}\in {I}⟼{F}\left({x}\right){M}{G}\left({x}\right)\right)=\left({x}\in {I}⟼{F}\left({x}\right){+}_{{R}}{inv}_{g}\left({R}\right)\left({G}\left({x}\right)\right)\right)$
37 27 33 36 3eqtr4d ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}{+}_{{Y}}{inv}_{g}\left({Y}\right)\left({G}\right)=\left({x}\in {I}⟼{F}\left({x}\right){M}{G}\left({x}\right)\right)$
38 2 32 15 4 grpsubval
40 5 10 19 12 20 offval2 ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}{{M}}_{f}{G}=\left({x}\in {I}⟼{F}\left({x}\right){M}{G}\left({x}\right)\right)$