Theorem xpsgrpsub

Description: Value of the subtraction operation in a binary structure product of groups. (Contributed by AV, 24-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$$
	xpsgrpsub.c	$$⊢\phi \to C\in X$$
	xpsgrpsub.d	$$⊢\phi \to D\in Y$$
	xpsgrpsub.m	$$⊢\underset{\dot{}}{·}={-}_R$$
	xpsgrpsub.n	$$⊢\underset{\dot{}}{\times }={-}_S$$
	xpsgrpsub.o	$$⊢\underset{\dot{}}{-}={-}_T$$
Assertion	xpsgrpsub	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{-}⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$

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		xpsgrpsub.c	$$⊢\phi \to C\in X$$
9		xpsgrpsub.d	$$⊢\phi \to D\in Y$$
10		xpsgrpsub.m	$$⊢\underset{\dot{}}{·}={-}_R$$
11		xpsgrpsub.n	$$⊢\underset{\dot{}}{\times }={-}_S$$
12		xpsgrpsub.o	$$⊢\underset{\dot{}}{-}={-}_T$$
13	2 10	grpsubcl	$$⊢\left(R\in \mathrm{Grp}\wedge A\in X\wedge C\in X\right)\to A\underset{\dot{}}{·}C\in X$$
14	4 6 8 13	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}C\in X$$
15	3 11	grpsubcl	$$⊢\left(S\in \mathrm{Grp}\wedge B\in Y\wedge D\in Y\right)\to B\underset{\dot{}}{\times }D\in Y$$
16	5 7 9 15	syl3anc	$$⊢\phi \to B\underset{\dot{}}{\times }D\in Y$$
17		eqid	$$⊢{+}_R={+}_R$$
18	2 17 4 14 8	grpcld	$$⊢\phi \to \left(A\underset{\dot{}}{·}C\right){+}_{R}C\in X$$
19		eqid	$$⊢{+}_S={+}_S$$
20	3 19 5 16 9	grpcld	$$⊢\phi \to \left(B\underset{\dot{}}{\times }D\right){+}_{S}D\in Y$$
21		eqid	$$⊢{+}_T={+}_T$$
22	1 2 3 4 5 14 16 8 9 18 20 17 19 21	xpsadd	$$⊢\phi \to ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩{+}_T⟨C,D⟩=⟨\left(A\underset{\dot{}}{·}C\right){+}_{R}C,\left(B\underset{\dot{}}{\times }D\right){+}_{S}D⟩$$
23	2 17 10	grpnpcan	$$⊢\left(R\in \mathrm{Grp}\wedge A\in X\wedge C\in X\right)\to \left(A\underset{\dot{}}{·}C\right){+}_{R}C=A$$
24	4 6 8 23	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{·}C\right){+}_{R}C=A$$
25	3 19 11	grpnpcan	$$⊢\left(S\in \mathrm{Grp}\wedge B\in Y\wedge D\in Y\right)\to \left(B\underset{\dot{}}{\times }D\right){+}_{S}D=B$$
26	5 7 9 25	syl3anc	$$⊢\phi \to \left(B\underset{\dot{}}{\times }D\right){+}_{S}D=B$$
27	24 26	opeq12d	$$⊢\phi \to ⟨\left(A\underset{\dot{}}{·}C\right){+}_{R}C,\left(B\underset{\dot{}}{\times }D\right){+}_{S}D⟩=⟨A,B⟩$$
28	22 27	eqtrd	$$⊢\phi \to ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩{+}_T⟨C,D⟩=⟨A,B⟩$$
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	8 9	opelxpd	$$⊢\phi \to ⟨C,D⟩\in \left(X\times Y\right)$$
35	34 32	eleqtrd	$$⊢\phi \to ⟨C,D⟩\in {\mathrm{Base}}_T$$
36	14 16	opelxpd	$$⊢\phi \to ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\in \left(X\times Y\right)$$
37	36 32	eleqtrd	$$⊢\phi \to ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\in {\mathrm{Base}}_T$$
38		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
39	38 21 12	grpsubadd	$$⊢\left(T\in \mathrm{Grp}\wedge \left(⟨A,B⟩\in {\mathrm{Base}}_T\wedge ⟨C,D⟩\in {\mathrm{Base}}_T\wedge ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\in {\mathrm{Base}}_T\right)\right)\to \left(⟨A,B⟩\underset{\dot{}}{-}⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\leftrightarrow ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩{+}_T⟨C,D⟩=⟨A,B⟩\right)$$
40	30 33 35 37 39	syl13anc	$$⊢\phi \to \left(⟨A,B⟩\underset{\dot{}}{-}⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩\leftrightarrow ⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩{+}_T⟨C,D⟩=⟨A,B⟩\right)$$
41	28 40	mpbird	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{-}⟨C,D⟩=⟨A\underset{\dot{}}{·}C,B\underset{\dot{}}{\times }D⟩$$