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 = {Base}_{R}$
	xpsinv.y	$⊢ Y = {Base}_{S}$
	xpsinv.r	$⊢ φ \to R \in Grp$
	xpsinv.s	$⊢ φ \to S \in Grp$
	xpsinv.a	$⊢ φ \to A \in X$
	xpsinv.b	$⊢ φ \to B \in Y$
	xpsgrpsub.c	$⊢ φ \to C \in X$
	xpsgrpsub.d	$⊢ φ \to D \in Y$
	xpsgrpsub.m	$⊢ \underset{˙}{\cdot} = -_{R}$
	xpsgrpsub.n	$⊢ \underset{˙}{\times} = -_{S}$
	xpsgrpsub.o	$⊢ \underset{˙}{-} = -_{T}$
Assertion	xpsgrpsub	$⊢ φ \to ⟨A, B⟩ \underset{˙}{-} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩$

Proof

Step	Hyp	Ref	Expression
1		xpsinv.t	$⊢ T = R \times_{𝑠} S$
2		xpsinv.x	$⊢ X = {Base}_{R}$
3		xpsinv.y	$⊢ Y = {Base}_{S}$
4		xpsinv.r	$⊢ φ \to R \in Grp$
5		xpsinv.s	$⊢ φ \to S \in Grp$
6		xpsinv.a	$⊢ φ \to A \in X$
7		xpsinv.b	$⊢ φ \to B \in Y$
8		xpsgrpsub.c	$⊢ φ \to C \in X$
9		xpsgrpsub.d	$⊢ φ \to D \in Y$
10		xpsgrpsub.m	$⊢ \underset{˙}{\cdot} = -_{R}$
11		xpsgrpsub.n	$⊢ \underset{˙}{\times} = -_{S}$
12		xpsgrpsub.o	$⊢ \underset{˙}{-} = -_{T}$
13	2 10	grpsubcl	$⊢ (R \in Grp \land A \in X \land C \in X) \to A \underset{˙}{\cdot} C \in X$
14	4 6 8 13	syl3anc	$⊢ φ \to A \underset{˙}{\cdot} C \in X$
15	3 11	grpsubcl	$⊢ (S \in Grp \land B \in Y \land D \in Y) \to B \underset{˙}{\times} D \in Y$
16	5 7 9 15	syl3anc	$⊢ φ \to B \underset{˙}{\times} D \in Y$
17		eqid	$⊢ +_{R} = +_{R}$
18	2 17 4 14 8	grpcld	$⊢ φ \to (A \underset{˙}{\cdot} C) +_{R} C \in X$
19		eqid	$⊢ +_{S} = +_{S}$
20	3 19 5 16 9	grpcld	$⊢ φ \to (B \underset{˙}{\times} D) +_{S} D \in Y$
21		eqid	$⊢ +_{T} = +_{T}$
22	1 2 3 4 5 14 16 8 9 18 20 17 19 21	xpsadd	$⊢ φ \to ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ +_{T} ⟨C, D⟩ = ⟨(A \underset{˙}{\cdot} C) +_{R} C, (B \underset{˙}{\times} D) +_{S} D⟩$
23	2 17 10	grpnpcan	$⊢ (R \in Grp \land A \in X \land C \in X) \to (A \underset{˙}{\cdot} C) +_{R} C = A$
24	4 6 8 23	syl3anc	$⊢ φ \to (A \underset{˙}{\cdot} C) +_{R} C = A$
25	3 19 11	grpnpcan	$⊢ (S \in Grp \land B \in Y \land D \in Y) \to (B \underset{˙}{\times} D) +_{S} D = B$
26	5 7 9 25	syl3anc	$⊢ φ \to (B \underset{˙}{\times} D) +_{S} D = B$
27	24 26	opeq12d	$⊢ φ \to ⟨(A \underset{˙}{\cdot} C) +_{R} C, (B \underset{˙}{\times} D) +_{S} D⟩ = ⟨A, B⟩$
28	22 27	eqtrd	$⊢ φ \to ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ +_{T} ⟨C, D⟩ = ⟨A, B⟩$
29	1	xpsgrp	$⊢ (R \in Grp \land S \in Grp) \to T \in Grp$
30	4 5 29	syl2anc	$⊢ φ \to T \in Grp$
31	6 7	opelxpd	$⊢ φ \to ⟨A, B⟩ \in (X \times Y)$
32	1 2 3 4 5	xpsbas	$⊢ φ \to X \times Y = {Base}_{T}$
33	31 32	eleqtrd	$⊢ φ \to ⟨A, B⟩ \in {Base}_{T}$
34	8 9	opelxpd	$⊢ φ \to ⟨C, D⟩ \in (X \times Y)$
35	34 32	eleqtrd	$⊢ φ \to ⟨C, D⟩ \in {Base}_{T}$
36	14 16	opelxpd	$⊢ φ \to ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ \in (X \times Y)$
37	36 32	eleqtrd	$⊢ φ \to ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ \in {Base}_{T}$
38		eqid	$⊢ {Base}_{T} = {Base}_{T}$
39	38 21 12	grpsubadd	$⊢ (T \in Grp \land (⟨A, B⟩ \in {Base}_{T} \land ⟨C, D⟩ \in {Base}_{T} \land ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ \in {Base}_{T})) \to (⟨A, B⟩ \underset{˙}{-} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ \leftrightarrow ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ +_{T} ⟨C, D⟩ = ⟨A, B⟩)$
40	30 33 35 37 39	syl13anc	$⊢ φ \to (⟨A, B⟩ \underset{˙}{-} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ \leftrightarrow ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩ +_{T} ⟨C, D⟩ = ⟨A, B⟩)$
41	28 40	mpbird	$⊢ φ \to ⟨A, B⟩ \underset{˙}{-} ⟨C, D⟩ = ⟨A \underset{˙}{\cdot} C, B \underset{˙}{\times} D⟩$

Metamath Proof Explorer

Theorem xpsgrpsub

Proof