# Metamath Proof Explorer

## Theorem pwsinvg

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

Ref Expression
Hypotheses pwsgrp.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
pwsinvg.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
pwsinvg.m ${⊢}{M}={inv}_{g}\left({R}\right)$
pwsinvg.n ${⊢}{N}={inv}_{g}\left({Y}\right)$
Assertion pwsinvg ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {N}\left({X}\right)={M}\circ {X}$

### Proof

Step Hyp Ref Expression
1 pwsgrp.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsinvg.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
3 pwsinvg.m ${⊢}{M}={inv}_{g}\left({R}\right)$
4 pwsinvg.n ${⊢}{N}={inv}_{g}\left({Y}\right)$
5 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
6 simp2 ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {I}\in {V}$
7 fvexd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
8 simp1 ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {R}\in \mathrm{Grp}$
9 fconst6g ${⊢}{R}\in \mathrm{Grp}\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Grp}$
10 8 9 syl ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Grp}$
11 eqid ${⊢}{\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
12 eqid ${⊢}{inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)={inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)$
13 simp3 ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {X}\in {B}$
14 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
15 1 14 pwsval ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
16 15 3adant3 ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
17 16 fveq2d ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
18 2 17 syl5eq ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {B}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
19 13 18 eleqtrd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {X}\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
20 5 6 7 10 11 12 19 prdsinvgd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)\left({X}\right)=\left({x}\in {I}⟼{inv}_{g}\left(\left({I}×\left\{{R}\right\}\right)\left({x}\right)\right)\left({X}\left({x}\right)\right)\right)$
21 fvconst2g ${⊢}\left({R}\in \mathrm{Grp}\wedge {x}\in {I}\right)\to \left({I}×\left\{{R}\right\}\right)\left({x}\right)={R}$
22 8 21 sylan ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\wedge {x}\in {I}\right)\to \left({I}×\left\{{R}\right\}\right)\left({x}\right)={R}$
23 22 fveq2d ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\wedge {x}\in {I}\right)\to {inv}_{g}\left(\left({I}×\left\{{R}\right\}\right)\left({x}\right)\right)={inv}_{g}\left({R}\right)$
24 23 3 eqtr4di ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\wedge {x}\in {I}\right)\to {inv}_{g}\left(\left({I}×\left\{{R}\right\}\right)\left({x}\right)\right)={M}$
25 24 fveq1d ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\wedge {x}\in {I}\right)\to {inv}_{g}\left(\left({I}×\left\{{R}\right\}\right)\left({x}\right)\right)\left({X}\left({x}\right)\right)={M}\left({X}\left({x}\right)\right)$
26 25 mpteq2dva ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to \left({x}\in {I}⟼{inv}_{g}\left(\left({I}×\left\{{R}\right\}\right)\left({x}\right)\right)\left({X}\left({x}\right)\right)\right)=\left({x}\in {I}⟼{M}\left({X}\left({x}\right)\right)\right)$
27 20 26 eqtrd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)\left({X}\right)=\left({x}\in {I}⟼{M}\left({X}\left({x}\right)\right)\right)$
28 16 fveq2d ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {inv}_{g}\left({Y}\right)={inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)$
29 4 28 syl5eq ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {N}={inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)$
30 29 fveq1d ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {N}\left({X}\right)={inv}_{g}\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)\left({X}\right)$
31 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
32 1 31 2 8 6 13 pwselbas ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {X}:{I}⟶{\mathrm{Base}}_{{R}}$
33 32 ffvelrnda ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\wedge {x}\in {I}\right)\to {X}\left({x}\right)\in {\mathrm{Base}}_{{R}}$
34 32 feqmptd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {X}=\left({x}\in {I}⟼{X}\left({x}\right)\right)$
35 31 3 grpinvf ${⊢}{R}\in \mathrm{Grp}\to {M}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
36 8 35 syl ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {M}:{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{R}}$
37 36 feqmptd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {M}=\left({y}\in {\mathrm{Base}}_{{R}}⟼{M}\left({y}\right)\right)$
38 fveq2 ${⊢}{y}={X}\left({x}\right)\to {M}\left({y}\right)={M}\left({X}\left({x}\right)\right)$
39 33 34 37 38 fmptco ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {M}\circ {X}=\left({x}\in {I}⟼{M}\left({X}\left({x}\right)\right)\right)$
40 27 30 39 3eqtr4d ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\wedge {X}\in {B}\right)\to {N}\left({X}\right)={M}\circ {X}$