This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsinvgd

Description: Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Hypotheses prdsgrpd.y 
|- Y = ( S Xs_ R )
prdsgrpd.i 
|- ( ph -> I e. W )
prdsgrpd.s 
|- ( ph -> S e. V )
prdsgrpd.r 
|- ( ph -> R : I --> Grp )
prdsinvgd.b 
|- B = ( Base ` Y )
prdsinvgd.n 
|- N = ( invg ` Y )
prdsinvgd.x 
|- ( ph -> X e. B )
Assertion prdsinvgd 
|- ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 prdsgrpd.y 
 |-  Y = ( S Xs_ R )
2 prdsgrpd.i 
 |-  ( ph -> I e. W )
3 prdsgrpd.s 
 |-  ( ph -> S e. V )
4 prdsgrpd.r 
 |-  ( ph -> R : I --> Grp )
5 prdsinvgd.b 
 |-  B = ( Base ` Y )
6 prdsinvgd.n 
 |-  N = ( invg ` Y )
7 prdsinvgd.x 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
9 3 elexd 
 |-  ( ph -> S e. _V )
10 2 elexd 
 |-  ( ph -> I e. _V )
11 eqid 
 |-  ( 0g o. R ) = ( 0g o. R )
12 eqid 
 |-  ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) )
13 1 5 8 9 10 4 7 11 12 prdsinvlem 
 |-  ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B /\ ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g o. R ) ) )
14 13 simprd 
 |-  ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g o. R ) )
15 grpmnd 
 |-  ( a e. Grp -> a e. Mnd )
16 15 ssriv 
 |-  Grp C_ Mnd
17 fss 
 |-  ( ( R : I --> Grp /\ Grp C_ Mnd ) -> R : I --> Mnd )
18 4 16 17 sylancl 
 |-  ( ph -> R : I --> Mnd )
19 1 2 3 18 prds0g 
 |-  ( ph -> ( 0g o. R ) = ( 0g ` Y ) )
20 14 19 eqtrd 
 |-  ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) )
21 1 2 3 4 prdsgrpd 
 |-  ( ph -> Y e. Grp )
22 13 simpld 
 |-  ( ph -> ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B )
23 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
24 5 8 23 6 grpinvid2 
 |-  ( ( Y e. Grp /\ X e. B /\ ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) e. B ) -> ( ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) <-> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) ) )
25 21 7 22 24 syl3anc 
 |-  ( ph -> ( ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) <-> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ( +g ` Y ) X ) = ( 0g ` Y ) ) )
26 20 25 mpbird 
 |-  ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) )