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 ^s I )
pwsinvg.b 
|- B = ( Base ` Y )
pwsinvg.m 
|- M = ( invg ` R )
pwsinvg.n 
|- N = ( invg ` Y )
Assertion pwsinvg 
|- ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( M o. X ) )

Proof

Step Hyp Ref Expression
1 pwsgrp.y 
 |-  Y = ( R ^s I )
2 pwsinvg.b 
 |-  B = ( Base ` Y )
3 pwsinvg.m 
 |-  M = ( invg ` R )
4 pwsinvg.n 
 |-  N = ( invg ` Y )
5 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
6 simp2 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> I e. V )
7 fvexd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( Scalar ` R ) e. _V )
8 simp1 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> R e. Grp )
9 fconst6g 
 |-  ( R e. Grp -> ( I X. { R } ) : I --> Grp )
10 8 9 syl 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( I X. { R } ) : I --> Grp )
11 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
12 eqid 
 |-  ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
13 simp3 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> X e. B )
14 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
15 1 14 pwsval 
 |-  ( ( R e. Grp /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
16 15 3adant3 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
17 16 fveq2d 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
18 2 17 eqtrid 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> B = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
19 13 18 eleqtrd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> X e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
20 5 6 7 10 11 12 19 prdsinvgd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ` X ) = ( x e. I |-> ( ( invg ` ( ( I X. { R } ) ` x ) ) ` ( X ` x ) ) ) )
21 fvconst2g 
 |-  ( ( R e. Grp /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
22 8 21 sylan 
 |-  ( ( ( R e. Grp /\ I e. V /\ X e. B ) /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
23 22 fveq2d 
 |-  ( ( ( R e. Grp /\ I e. V /\ X e. B ) /\ x e. I ) -> ( invg ` ( ( I X. { R } ) ` x ) ) = ( invg ` R ) )
24 23 3 eqtr4di 
 |-  ( ( ( R e. Grp /\ I e. V /\ X e. B ) /\ x e. I ) -> ( invg ` ( ( I X. { R } ) ` x ) ) = M )
25 24 fveq1d 
 |-  ( ( ( R e. Grp /\ I e. V /\ X e. B ) /\ x e. I ) -> ( ( invg ` ( ( I X. { R } ) ` x ) ) ` ( X ` x ) ) = ( M ` ( X ` x ) ) )
26 25 mpteq2dva 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( x e. I |-> ( ( invg ` ( ( I X. { R } ) ` x ) ) ` ( X ` x ) ) ) = ( x e. I |-> ( M ` ( X ` x ) ) ) )
27 20 26 eqtrd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ` X ) = ( x e. I |-> ( M ` ( X ` x ) ) ) )
28 16 fveq2d 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( invg ` Y ) = ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
29 4 28 eqtrid 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> N = ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
30 29 fveq1d 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( ( invg ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) ` X ) )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 1 31 2 8 6 13 pwselbas 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> X : I --> ( Base ` R ) )
33 32 ffvelcdmda 
 |-  ( ( ( R e. Grp /\ I e. V /\ X e. B ) /\ x e. I ) -> ( X ` x ) e. ( Base ` R ) )
34 32 feqmptd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> X = ( x e. I |-> ( X ` x ) ) )
35 31 3 grpinvf 
 |-  ( R e. Grp -> M : ( Base ` R ) --> ( Base ` R ) )
36 8 35 syl 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> M : ( Base ` R ) --> ( Base ` R ) )
37 36 feqmptd 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> M = ( y e. ( Base ` R ) |-> ( M ` y ) ) )
38 fveq2 
 |-  ( y = ( X ` x ) -> ( M ` y ) = ( M ` ( X ` x ) ) )
39 33 34 37 38 fmptco 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( M o. X ) = ( x e. I |-> ( M ` ( X ` x ) ) ) )
40 27 30 39 3eqtr4d 
 |-  ( ( R e. Grp /\ I e. V /\ X e. B ) -> ( N ` X ) = ( M o. X ) )