This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpsmnd0

Description: The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025)

Ref Expression
Hypothesis xpsmnd0.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
Assertion xpsmnd0 ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 0g ‘ 𝑇 ) = ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ )

Proof

Step Hyp Ref Expression
1 xpsmnd0.t ⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
4 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 5 6 mndidcl ⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
8 7 adantr ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
9 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
11 9 10 mndidcl ⊢ ( 𝑆 ∈ Mnd → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
12 11 adantl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
13 8 12 opelxpd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ∈ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) )
14 simpl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → 𝑅 ∈ Mnd )
15 simpr ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → 𝑆 ∈ Mnd )
16 1 5 9 14 15 xpsbas ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) = ( Base ‘ 𝑇 ) )
17 13 16 eleqtrd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ∈ ( Base ‘ 𝑇 ) )
18 16 eleq2d ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝑇 ) ) )
19 elxp2 ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ∃ 𝑏 ∈ ( Base ‘ 𝑆 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
20 14 adantr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Mnd )
21 15 adantr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑆 ∈ Mnd )
22 8 adantr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
23 12 adantr ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
24 simpl ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
25 24 adantl ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
26 simpr ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
27 26 adantl ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
28 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
29 5 28 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
30 20 22 25 29 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
31 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
32 9 31 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
33 21 23 27 32 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
34 1 5 9 20 21 22 23 25 27 30 33 28 31 4 xpsadd ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) , ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) ⟩ )
35 5 28 6 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) = 𝑎 )
36 14 24 35 syl2an ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) = 𝑎 )
37 9 31 10 mndlid ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 )
38 15 26 37 syl2an ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 )
39 36 38 opeq12d ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ⟨ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑎 ) , ( ( 0g ‘ 𝑆 ) ( +g ‘ 𝑆 ) 𝑏 ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
40 34 39 eqtrd ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ )
41 oveq2 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
42 id ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
43 41 42 eqeq12d ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 ↔ ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
44 40 43 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 ) )
45 44 rexlimdvva ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ∃ 𝑏 ∈ ( Base ‘ 𝑆 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 ) )
46 19 45 biimtrid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 ) )
47 18 46 sylbird ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑥 ∈ ( Base ‘ 𝑇 ) → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 ) )
48 47 imp ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ( +g ‘ 𝑇 ) 𝑥 ) = 𝑥 )
49 5 28 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
50 20 25 22 49 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
51 9 31 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) ∈ ( Base ‘ 𝑆 ) )
52 21 27 23 51 syl3anc ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) ∈ ( Base ‘ 𝑆 ) )
53 1 5 9 20 21 25 27 22 23 50 52 28 31 4 xpsadd ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = ⟨ ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) , ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) ⟩ )
54 5 28 6 mndrid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = 𝑎 )
55 14 24 54 syl2an ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = 𝑎 )
56 9 31 10 mndrid ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) = 𝑏 )
57 15 26 56 syl2an ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) = 𝑏 )
58 55 57 opeq12d ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ⟨ ( 𝑎 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) , ( 𝑏 ( +g ‘ 𝑆 ) ( 0g ‘ 𝑆 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
59 53 58 eqtrd ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ )
60 oveq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) )
61 60 42 eqeq12d ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
62 59 61 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 ) )
63 62 rexlimdvva ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ∃ 𝑏 ∈ ( Base ‘ 𝑆 ) 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 ) )
64 19 63 biimtrid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 ) )
65 18 64 sylbird ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑥 ∈ ( Base ‘ 𝑇 ) → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 ) )
66 65 imp ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( 𝑥 ( +g ‘ 𝑇 ) ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ ) = 𝑥 )
67 2 3 4 17 48 66 ismgmid2 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ = ( 0g ‘ 𝑇 ) )
68 67 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 0g ‘ 𝑇 ) = ⟨ ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑆 ) ⟩ )