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

Metamath Proof Explorer

Theorem 0ringcring

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

Ref Expression
Hypotheses 0ringcring.1 ⊢ B = Base R
0ringcring.2 ⊢ φ → R ∈ Ring
0ringcring.3 ⊢ φ → B = 1
Assertion 0ringcring ⊢ φ → R ∈ CRing

Proof

Step Hyp Ref Expression
1 0ringcring.1 ⊢ B = Base R
2 0ringcring.2 ⊢ φ → R ∈ Ring
3 0ringcring.3 ⊢ φ → B = 1
4 eqid ⊢ mulGrp R = mulGrp R
5 4 1 mgpbas ⊢ B = Base mulGrp R
6 5 a1i ⊢ φ → B = Base mulGrp R
7 eqid ⊢ ⋅ R = ⋅ R
8 4 7 mgpplusg ⊢ ⋅ R = + mulGrp R
9 8 a1i ⊢ φ → ⋅ R = + mulGrp R
10 4 ringmgp ⊢ R ∈ Ring → mulGrp R ∈ Mnd
11 2 10 syl ⊢ φ → mulGrp R ∈ Mnd
12 eqid ⊢ 0 R = 0 R
13 2 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → R ∈ Ring
14 simp3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ B
15 1 7 12 13 14 ringlzd ⊢ φ ∧ x ∈ B ∧ y ∈ B → 0 R ⋅ R y = 0 R
16 1 7 12 13 14 ringrzd ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ⋅ R 0 R = 0 R
17 15 16 eqtr4d ⊢ φ ∧ x ∈ B ∧ y ∈ B → 0 R ⋅ R y = y ⋅ R 0 R
18 simp2 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ B
19 1 12 0ring ⊢ R ∈ Ring ∧ B = 1 → B = 0 R
20 2 3 19 syl2anc ⊢ φ → B = 0 R
21 20 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → B = 0 R
22 18 21 eleqtrd ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ 0 R
23 elsni ⊢ x ∈ 0 R → x = 0 R
24 22 23 syl ⊢ φ ∧ x ∈ B ∧ y ∈ B → x = 0 R
25 24 oveq1d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ R y = 0 R ⋅ R y
26 24 oveq2d ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ⋅ R x = y ⋅ R 0 R
27 17 25 26 3eqtr4d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ R y = y ⋅ R x
28 6 9 11 27 iscmnd ⊢ φ → mulGrp R ∈ CMnd
29 4 iscrng ⊢ R ∈ CRing ↔ R ∈ Ring ∧ mulGrp R ∈ CMnd
30 2 28 29 sylanbrc ⊢ φ → R ∈ CRing