Theorem xpsinv

Description: Value of the negation operation in a binary structure product. (Contributed by AV, 18-Mar-2025)

	Ref	Expression
Hypotheses	xpsinv.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsinv.x	$$⊢X={\mathrm{Base}}_R$$
	xpsinv.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsinv.r	$$⊢\phi \to R\in \mathrm{Grp}$$
	xpsinv.s	$$⊢\phi \to S\in \mathrm{Grp}$$
	xpsinv.a	$$⊢\phi \to A\in X$$
	xpsinv.b	$$⊢\phi \to B\in Y$$
	xpsinv.m	$$⊢M={inv}_g\left(R\right)$$
	xpsinv.n	$$⊢N={inv}_g\left(S\right)$$
	xpsinv.i	$$⊢I={inv}_g\left(T\right)$$
Assertion	xpsinv	$$⊢\phi \to I\left(⟨A,B⟩\right)=⟨M\left(A\right),N\left(B\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		xpsinv.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsinv.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsinv.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsinv.r	$$⊢\phi \to R\in \mathrm{Grp}$$
5		xpsinv.s	$$⊢\phi \to S\in \mathrm{Grp}$$
6		xpsinv.a	$$⊢\phi \to A\in X$$
7		xpsinv.b	$$⊢\phi \to B\in Y$$
8		xpsinv.m	$$⊢M={inv}_g\left(R\right)$$
9		xpsinv.n	$$⊢N={inv}_g\left(S\right)$$
10		xpsinv.i	$$⊢I={inv}_g\left(T\right)$$
11		eqid	$$⊢{+}_R={+}_R$$
12		eqid	$$⊢0_R=0_R$$
13	2 11 12 8 4 6	grplinvd	$$⊢\phi \to M\left(A\right){+}_{R}A=0_R$$
14		eqid	$$⊢{+}_S={+}_S$$
15		eqid	$$⊢0_S=0_S$$
16	3 14 15 9 5 7	grplinvd	$$⊢\phi \to N\left(B\right){+}_{S}B=0_S$$
17	13 16	opeq12d	$$⊢\phi \to ⟨M\left(A\right){+}_{R}A,N\left(B\right){+}_{S}B⟩=⟨0_R,0_S⟩$$
18	2 8 4 6	grpinvcld	$$⊢\phi \to M\left(A\right)\in X$$
19	3 9 5 7	grpinvcld	$$⊢\phi \to N\left(B\right)\in Y$$
20	2 11 4 18 6	grpcld	$$⊢\phi \to M\left(A\right){+}_{R}A\in X$$
21	3 14 5 19 7	grpcld	$$⊢\phi \to N\left(B\right){+}_{S}B\in Y$$
22		eqid	$$⊢{+}_T={+}_T$$
23	1 2 3 4 5 18 19 6 7 20 21 11 14 22	xpsadd	$$⊢\phi \to ⟨M\left(A\right),N\left(B\right)⟩{+}_T⟨A,B⟩=⟨M\left(A\right){+}_{R}A,N\left(B\right){+}_{S}B⟩$$
24	4	grpmndd	$$⊢\phi \to R\in \mathrm{Mnd}$$
25	5	grpmndd	$$⊢\phi \to S\in \mathrm{Mnd}$$
26	1	xpsmnd0	$$⊢\left(R\in \mathrm{Mnd}\wedge S\in \mathrm{Mnd}\right)\to 0_T=⟨0_R,0_S⟩$$
27	24 25 26	syl2anc	$$⊢\phi \to 0_T=⟨0_R,0_S⟩$$
28	17 23 27	3eqtr4d	$$⊢\phi \to ⟨M\left(A\right),N\left(B\right)⟩{+}_T⟨A,B⟩=0_T$$
29	1	xpsgrp	$$⊢\left(R\in \mathrm{Grp}\wedge S\in \mathrm{Grp}\right)\to T\in \mathrm{Grp}$$
30	4 5 29	syl2anc	$$⊢\phi \to T\in \mathrm{Grp}$$
31	6 7	opelxpd	$$⊢\phi \to ⟨A,B⟩\in \left(X\times Y\right)$$
32	1 2 3 4 5	xpsbas	$$⊢\phi \to X\times Y={\mathrm{Base}}_T$$
33	31 32	eleqtrd	$$⊢\phi \to ⟨A,B⟩\in {\mathrm{Base}}_T$$
34	18 19	opelxpd	$$⊢\phi \to ⟨M\left(A\right),N\left(B\right)⟩\in \left(X\times Y\right)$$
35	34 32	eleqtrd	$$⊢\phi \to ⟨M\left(A\right),N\left(B\right)⟩\in {\mathrm{Base}}_T$$
36		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
37		eqid	$$⊢0_T=0_T$$
38	36 22 37 10	grpinvid2	$$⊢\left(T\in \mathrm{Grp}\wedge ⟨A,B⟩\in {\mathrm{Base}}_T\wedge ⟨M\left(A\right),N\left(B\right)⟩\in {\mathrm{Base}}_T\right)\to \left(I\left(⟨A,B⟩\right)=⟨M\left(A\right),N\left(B\right)⟩\leftrightarrow ⟨M\left(A\right),N\left(B\right)⟩{+}_T⟨A,B⟩=0_T\right)$$
39	30 33 35 38	syl3anc	$$⊢\phi \to \left(I\left(⟨A,B⟩\right)=⟨M\left(A\right),N\left(B\right)⟩\leftrightarrow ⟨M\left(A\right),N\left(B\right)⟩{+}_T⟨A,B⟩=0_T\right)$$
40	28 39	mpbird	$$⊢\phi \to I\left(⟨A,B⟩\right)=⟨M\left(A\right),N\left(B\right)⟩$$