Metamath Proof Explorer

Theorem iscrngd

Description: Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses isringd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
isringd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
isringd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
isringd.g ⊢ ( 𝜑 → 𝑅 ∈ Grp )
isringd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
isringd.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
isringd.d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
isringd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
isringd.u ⊢ ( 𝜑 → 1 ∈ 𝐵 )
isringd.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
isringd.h ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
iscrngd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
Assertion iscrngd ( 𝜑 → 𝑅 ∈ CRing )

Proof

Step Hyp Ref Expression
1 isringd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2 isringd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
3 isringd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
4 isringd.g ⊢ ( 𝜑 → 𝑅 ∈ Grp )
5 isringd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
6 isringd.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
7 isringd.d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
8 isringd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
9 isringd.u ⊢ ( 𝜑 → 1 ∈ 𝐵 )
10 isringd.i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
11 isringd.h ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 1 ) = 𝑥 )
12 iscrngd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
13 1 2 3 4 5 6 7 8 9 10 11 isringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
14 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 14 15 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17 1 16 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
18 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19 14 18 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
20 3 19 eqtrdi ⊢ ( 𝜑 → · = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
21 17 20 5 6 9 10 11 ismndd ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
22 17 20 21 12 iscmnd ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
23 14 iscrng ⊢ ( 𝑅 ∈ CRing ↔ ( 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ CMnd ) )
24 13 22 23 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ CRing )