Metamath Proof Explorer

Theorem srg1zr

Description: The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 19-Jun-2026)

Ref Expression
Hypotheses srg1zr.b 
|- B = ( Base ` R )
srg1zr.p 
|- .+ = ( +g ` R )
srg1zr.t 
|- .* = ( .r ` R )
Assertion srg1zr 
|- ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )

Proof

Step Hyp Ref Expression
1 srg1zr.b 
 |-  B = ( Base ` R )
2 srg1zr.p 
 |-  .+ = ( +g ` R )
3 srg1zr.t 
 |-  .* = ( .r ` R )
4 srgmnd 
 |-  ( R e. SRing -> R e. Mnd )
5 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
6 4 5 syl 
 |-  ( R e. SRing -> R e. Mgm )
7 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
8 7 srgmgp 
 |-  ( R e. SRing -> ( mulGrp ` R ) e. Mnd )
9 mndmgm 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Mgm )
10 8 9 syl 
 |-  ( R e. SRing -> ( mulGrp ` R ) e. Mgm )
11 6 10 jca 
 |-  ( R e. SRing -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
12 11 3ad2ant1 
 |-  ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
13 12 adantr 
 |-  ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
14 3simpc 
 |-  ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) )
15 14 adantr 
 |-  ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) )
16 simpr 
 |-  ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> Z e. B )
17 1 2 3 rng1zrlem 
 |-  ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18 13 15 16 17 syl3anc 
 |-  ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )