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 ) ) ) )