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 
|- ( ph -> R e. Ring )
0ringcring.3 
|- ( ph -> ( # ` B ) = 1 )
Assertion 0ringcring 
|- ( ph -> R e. CRing )

Proof

Step Hyp Ref Expression
1 0ringcring.1 
 |-  B = ( Base ` R )
2 0ringcring.2 
 |-  ( ph -> R e. Ring )
3 0ringcring.3 
 |-  ( ph -> ( # ` B ) = 1 )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 4 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
6 5 a1i 
 |-  ( ph -> B = ( Base ` ( mulGrp ` R ) ) )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 4 7 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
9 8 a1i 
 |-  ( ph -> ( .r ` R ) = ( +g ` ( mulGrp ` R ) ) )
10 4 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
11 2 10 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 2 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> R e. Ring )
14 simp3 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> y e. B )
15 1 7 12 13 14 ringlzd 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( 0g ` R ) ( .r ` R ) y ) = ( 0g ` R ) )
16 1 7 12 13 14 ringrzd 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( y ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
17 15 16 eqtr4d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( 0g ` R ) ( .r ` R ) y ) = ( y ( .r ` R ) ( 0g ` R ) ) )
18 simp2 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> x e. B )
19 1 12 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { ( 0g ` R ) } )
20 2 3 19 syl2anc 
 |-  ( ph -> B = { ( 0g ` R ) } )
21 20 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> B = { ( 0g ` R ) } )
22 18 21 eleqtrd 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> x e. { ( 0g ` R ) } )
23 elsni 
 |-  ( x e. { ( 0g ` R ) } -> x = ( 0g ` R ) )
24 22 23 syl 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> x = ( 0g ` R ) )
25 24 oveq1d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x ( .r ` R ) y ) = ( ( 0g ` R ) ( .r ` R ) y ) )
26 24 oveq2d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( y ( .r ` R ) x ) = ( y ( .r ` R ) ( 0g ` R ) ) )
27 17 25 26 3eqtr4d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x ( .r ` R ) y ) = ( y ( .r ` R ) x ) )
28 6 9 11 27 iscmnd 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
29 4 iscrng 
 |-  ( R e. CRing <-> ( R e. Ring /\ ( mulGrp ` R ) e. CMnd ) )
30 2 28 29 sylanbrc 
 |-  ( ph -> R e. CRing )