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 𝑠 R
prdsgrpd.i φ I W
prdsgrpd.s φ S V
prdsgrpd.r φ R : I Grp
prdsinvgd.b B = Base Y
prdsinvgd.n N = inv g Y
prdsinvgd.x φ X B
Assertion prdsinvgd φ N X = x I inv g R x X x

Proof

Step Hyp Ref Expression
1 prdsgrpd.y Y = S 𝑠 R
2 prdsgrpd.i φ I W
3 prdsgrpd.s φ S V
4 prdsgrpd.r φ R : I Grp
5 prdsinvgd.b B = Base Y
6 prdsinvgd.n N = inv g Y
7 prdsinvgd.x φ X B
8 eqid + Y = + Y
9 3 elexd φ S V
10 2 elexd φ I V
11 eqid 0 𝑔 R = 0 𝑔 R
12 eqid x I inv g R x X x = x I inv g R x X x
13 1 5 8 9 10 4 7 11 12 prdsinvlem φ x I inv g R x X x B x I inv g R x X x + Y X = 0 𝑔 R
14 13 simprd φ x I inv g R x X x + Y X = 0 𝑔 R
15 grpmnd a Grp a Mnd
16 15 ssriv Grp Mnd
17 fss R : I Grp Grp Mnd R : I Mnd
18 4 16 17 sylancl φ R : I Mnd
19 1 2 3 18 prds0g φ 0 𝑔 R = 0 Y
20 14 19 eqtrd φ x I inv g R x X x + Y X = 0 Y
21 1 2 3 4 prdsgrpd φ Y Grp
22 13 simpld φ x I inv g R x X x B
23 eqid 0 Y = 0 Y
24 5 8 23 6 grpinvid2 Y Grp X B x I inv g R x X x B N X = x I inv g R x X x x I inv g R x X x + Y X = 0 Y
25 21 7 22 24 syl3anc φ N X = x I inv g R x X x x I inv g R x X x + Y X = 0 Y
26 20 25 mpbird φ N X = x I inv g R x X x