Metamath Proof Explorer

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 ⊢ 𝑇 = ( 𝑅 ×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 ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ − ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 · 𝐶 ) , ( 𝐵 × 𝐷 ) ⟩ )