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	$$⊢\phi \to I\in W$$
	prdsgrpd.s	$$⊢\phi \to S\in V$$
	prdsgrpd.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
	prdsinvgd.b	$$⊢B={\mathrm{Base}}_Y$$
	prdsinvgd.n	$$⊢N={inv}_g\left(Y\right)$$
	prdsinvgd.x	$$⊢\phi \to X\in B$$
Assertion	prdsinvgd	$$⊢\phi \to N\left(X\right)=\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsgrpd.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsgrpd.i	$$⊢\phi \to I\in W$$
3		prdsgrpd.s	$$⊢\phi \to S\in V$$
4		prdsgrpd.r	$$⊢\phi \to R:I⟶\mathrm{Grp}$$
5		prdsinvgd.b	$$⊢B={\mathrm{Base}}_Y$$
6		prdsinvgd.n	$$⊢N={inv}_g\left(Y\right)$$
7		prdsinvgd.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢{+}_Y={+}_Y$$
9	3	elexd	$$⊢\phi \to S\in \mathrm{V}$$
10	2	elexd	$$⊢\phi \to I\in \mathrm{V}$$
11		eqid	$$⊢0_{𝑔}\circ R=0_{𝑔}\circ R$$
12		eqid	$$⊢\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)=\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)$$
13	1 5 8 9 10 4 7 11 12	prdsinvlem	$$⊢\phi \to \left(\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)\in B\wedge \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right){+}_{Y}X=0_{𝑔}\circ R\right)$$
14	13	simprd	$$⊢\phi \to \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right){+}_{Y}X=0_{𝑔}\circ R$$
15		grpmnd	$$⊢a\in \mathrm{Grp}\to a\in \mathrm{Mnd}$$
16	15	ssriv	$$⊢\mathrm{Grp}\subseteq \mathrm{Mnd}$$
17		fss	$$⊢\left(R:I⟶\mathrm{Grp}\wedge \mathrm{Grp}\subseteq \mathrm{Mnd}\right)\to R:I⟶\mathrm{Mnd}$$
18	4 16 17	sylancl	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
19	1 2 3 18	prds0g	$$⊢\phi \to 0_{𝑔}\circ R=0_Y$$
20	14 19	eqtrd	$$⊢\phi \to \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right){+}_{Y}X=0_Y$$
21	1 2 3 4	prdsgrpd	$$⊢\phi \to Y\in \mathrm{Grp}$$
22	13	simpld	$$⊢\phi \to \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)\in B$$
23		eqid	$$⊢0_Y=0_Y$$
24	5 8 23 6	grpinvid2	$$⊢\left(Y\in \mathrm{Grp}\wedge X\in B\wedge \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)\in B\right)\to \left(N\left(X\right)=\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)\leftrightarrow \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right){+}_{Y}X=0_Y\right)$$
25	21 7 22 24	syl3anc	$$⊢\phi \to \left(N\left(X\right)=\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)\leftrightarrow \left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right){+}_{Y}X=0_Y\right)$$
26	20 25	mpbird	$$⊢\phi \to N\left(X\right)=\left(x\in I⟼{inv}_g\left(R\left(x\right)\right)\left(X\left(x\right)\right)\right)$$