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	⊢ 𝑇 = ( 𝑅 ×_s 𝑆 )
	xpsinv.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	xpsinv.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
	xpsinv.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	xpsinv.s	⊢ ( 𝜑 → 𝑆 ∈ Grp )
	xpsinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	xpsinv.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
	xpsgrpsub.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	xpsgrpsub.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	xpsgrpsub.m	⊢ · = ( -_g ‘ 𝑅 )
	xpsgrpsub.n	⊢ × = ( -_g ‘ 𝑆 )
	xpsgrpsub.o	⊢ − = ( -_g ‘ 𝑇 )
Assertion	xpsgrpsub	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ − ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		xpsinv.t	⊢ 𝑇 = ( 𝑅 ×_s 𝑆 )
2		xpsinv.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
3		xpsinv.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
4		xpsinv.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
5		xpsinv.s	⊢ ( 𝜑 → 𝑆 ∈ Grp )
6		xpsinv.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
7		xpsinv.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
8		xpsgrpsub.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
9		xpsgrpsub.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
10		xpsgrpsub.m	⊢ · = ( -_g ‘ 𝑅 )
11		xpsgrpsub.n	⊢ × = ( -_g ‘ 𝑆 )
12		xpsgrpsub.o	⊢ − = ( -_g ‘ 𝑇 )
13	2 10	grpsubcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 · 𝐶 ) ∈ 𝑋 )
14	4 6 8 13	syl3anc	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ 𝑋 )
15	3 11	grpsubcl	⊢ ( ( 𝑆 ∈ Grp ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌 ) → ( 𝐵 × 𝐷 ) ∈ 𝑌 )
16	5 7 9 15	syl3anc	⊢ ( 𝜑 → ( 𝐵 × 𝐷 ) ∈ 𝑌 )
17		eqid	⊢ ( +_g ‘ 𝑅 ) = ( +_g ‘ 𝑅 )
18	2 17 4 14 8	grpcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) ( +_g ‘ 𝑅 ) 𝐶 ) ∈ 𝑋 )
19		eqid	⊢ ( +_g ‘ 𝑆 ) = ( +_g ‘ 𝑆 )
20	3 19 5 16 9	grpcld	⊢ ( 𝜑 → ( ( 𝐵 × 𝐷 ) ( +_g ‘ 𝑆 ) 𝐷 ) ∈ 𝑌 )
21		eqid	⊢ ( +_g ‘ 𝑇 ) = ( +_g ‘ 𝑇 )
22	1 2 3 4 5 14 16 8 9 18 20 17 19 21	xpsadd	⊢ ( 𝜑 → ( ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ( +_g ‘ 𝑇 ) ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 · 𝐶 ) ( +_g ‘ 𝑅 ) 𝐶 ) , ( ( 𝐵 × 𝐷 ) ( +_g ‘ 𝑆 ) 𝐷 ) ⟩ )
23	2 17 10	grpnpcan	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 · 𝐶 ) ( +_g ‘ 𝑅 ) 𝐶 ) = 𝐴 )
24	4 6 8 23	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) ( +_g ‘ 𝑅 ) 𝐶 ) = 𝐴 )
25	3 19 11	grpnpcan	⊢ ( ( 𝑆 ∈ Grp ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌 ) → ( ( 𝐵 × 𝐷 ) ( +_g ‘ 𝑆 ) 𝐷 ) = 𝐵 )
26	5 7 9 25	syl3anc	⊢ ( 𝜑 → ( ( 𝐵 × 𝐷 ) ( +_g ‘ 𝑆 ) 𝐷 ) = 𝐵 )
27	24 26	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 𝐴 · 𝐶 ) ( +_g ‘ 𝑅 ) 𝐶 ) , ( ( 𝐵 × 𝐷 ) ( +_g ‘ 𝑆 ) 𝐷 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
28	22 27	eqtrd	⊢ ( 𝜑 → ( ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ( +_g ‘ 𝑇 ) ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ )
29	1	xpsgrp	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑆 ∈ Grp ) → 𝑇 ∈ Grp )
30	4 5 29	syl2anc	⊢ ( 𝜑 → 𝑇 ∈ Grp )
31	6 7	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
32	1 2 3 4 5	xpsbas	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 ) )
33	31 32	eleqtrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( Base ‘ 𝑇 ) )
34	8 9	opelxpd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) )
35	34 32	eleqtrd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( Base ‘ 𝑇 ) )
36	14 16	opelxpd	⊢ ( 𝜑 → ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
37	36 32	eleqtrd	⊢ ( 𝜑 → ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ∈ ( Base ‘ 𝑇 ) )
38		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
39	38 21 12	grpsubadd	⊢ ( ( 𝑇 ∈ Grp ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( Base ‘ 𝑇 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( Base ‘ 𝑇 ) ∧ ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ∈ ( Base ‘ 𝑇 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ − ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ↔ ( ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ( +_g ‘ 𝑇 ) ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
40	30 33 35 37 39	syl13anc	⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ − ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ↔ ( ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ ( +_g ‘ 𝑇 ) ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
41	28 40	mpbird	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ − ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )

Metamath Proof Explorer

Theorem xpsgrpsub

Proof