Metamath Proof Explorer

Theorem 0ringcring

Description: The zero ring is commutative. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses 0ringcring.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
0ringcring.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
0ringcring.3 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
Assertion 0ringcring ( 𝜑 → 𝑅 ∈ CRing )

Proof

Step Hyp Ref Expression
1 0ringcring.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 0ringcring.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 0ringcring.3 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 4 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
6 5 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 4 7 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
9 8 a1i ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
10 4 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
11 2 10 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ Ring )
14 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
15 1 7 12 13 14 ringlzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) )
16 1 7 12 13 14 ringrzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
17 15 16 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
18 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
19 1 12 0ring ⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
20 2 3 19 syl2anc ⊢ ( 𝜑 → 𝐵 = { ( 0g ‘ 𝑅 ) } )
21 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
22 18 21 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ { ( 0g ‘ 𝑅 ) } )
23 elsni ⊢ ( 𝑥 ∈ { ( 0g ‘ 𝑅 ) } → 𝑥 = ( 0g ‘ 𝑅 ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = ( 0g ‘ 𝑅 ) )
25 24 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) )
26 24 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
27 17 25 26 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
28 6 9 11 27 iscmnd ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
29 4 iscrng ⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ CMnd ) )
30 2 28 29 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ CRing )