Metamath Proof Explorer

Theorem xpsinv

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

Ref Expression
Hypotheses xpsinv.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
xpsinv.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
xpsinv.y ⊢ 𝑌 = ( Base ‘ 𝑆 )
xpsinv.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
xpsinv.s ⊢ ( 𝜑 → 𝑆 ∈ Grp )
xpsinv.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
xpsinv.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
xpsinv.m ⊢ 𝑀 = ( invg ‘ 𝑅 )
xpsinv.n ⊢ 𝑁 = ( invg ‘ 𝑆 )
xpsinv.i ⊢ 𝐼 = ( invg ‘ 𝑇 )
Assertion xpsinv ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ )

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 xpsinv.m ⊢ 𝑀 = ( invg ‘ 𝑅 )
9 xpsinv.n ⊢ 𝑁 = ( invg ‘ 𝑆 )
10 xpsinv.i ⊢ 𝐼 = ( invg ‘ 𝑇 )
11 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 2 11 12 8 4 6 grplinvd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ( +g ‘ 𝑅 ) 𝐴 ) = ( 0g ‘ 𝑅 ) )
14 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
15 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
16 3 14 15 9 5 7 grplinvd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑆 ) 𝐵 ) = ( 0g ‘ 𝑆 ) )
17 13 16 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 𝑀 ‘ 𝐴 ) ( +g ‘ 𝑅 ) 𝐴 ) , ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑆 ) 𝐵 ) ⟩ = ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ )
18 2 8 4 6 grpinvcld ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑋 )
19 3 9 5 7 grpinvcld ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) ∈ 𝑌 )
20 2 11 4 18 6 grpcld ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ( +g ‘ 𝑅 ) 𝐴 ) ∈ 𝑋 )
21 3 14 5 19 7 grpcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑆 ) 𝐵 ) ∈ 𝑌 )
22 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
23 1 2 3 4 5 18 19 6 7 20 21 11 14 22 xpsadd ⊢ ( 𝜑 → ( ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ ( ( 𝑀 ‘ 𝐴 ) ( +g ‘ 𝑅 ) 𝐴 ) , ( ( 𝑁 ‘ 𝐵 ) ( +g ‘ 𝑆 ) 𝐵 ) ⟩ )
24 4 grpmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
25 5 grpmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
26 1 xpsmnd0 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 0g ‘ 𝑇 ) = ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ )
27 24 25 26 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑇 ) = ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ )
28 17 23 27 3eqtr4d ⊢ ( 𝜑 → ( ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝐴 , 𝐵 ⟩ ) = ( 0g ‘ 𝑇 ) )
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 18 19 opelxpd ⊢ ( 𝜑 → ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
35 34 32 eleqtrd ⊢ ( 𝜑 → ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ∈ ( Base ‘ 𝑇 ) )
36 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
37 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
38 36 22 37 10 grpinvid2 ⊢ ( ( 𝑇 ∈ Grp ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( Base ‘ 𝑇 ) ∧ ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝐼 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ↔ ( ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝐴 , 𝐵 ⟩ ) = ( 0g ‘ 𝑇 ) ) )
39 30 33 35 38 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ↔ ( ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝐴 , 𝐵 ⟩ ) = ( 0g ‘ 𝑇 ) ) )
40 28 39 mpbird ⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ ( 𝑀 ‘ 𝐴 ) , ( 𝑁 ‘ 𝐵 ) ⟩ )