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)

Ref Expression
Hypotheses srg1zr.b 𝐵 = ( Base ‘ 𝑅 )
srg1zr.p + = ( +g𝑅 )
srg1zr.t = ( .r𝑅 )
Assertion srg1zr ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 srg1zr.b 𝐵 = ( Base ‘ 𝑅 )
2 srg1zr.p + = ( +g𝑅 )
3 srg1zr.t = ( .r𝑅 )
4 pm4.24 ( 𝐵 = { 𝑍 } ↔ ( 𝐵 = { 𝑍 } ∧ 𝐵 = { 𝑍 } ) )
5 srgmnd ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
6 5 3ad2ant1 ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) → 𝑅 ∈ Mnd )
7 6 adantr ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → 𝑅 ∈ Mnd )
8 mndmgm ( 𝑅 ∈ Mnd → 𝑅 ∈ Mgm )
9 7 8 syl ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → 𝑅 ∈ Mgm )
10 simpr ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → 𝑍𝐵 )
11 simpl2 ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → + Fn ( 𝐵 × 𝐵 ) )
12 1 2 mgmb1mgm1 ( ( 𝑅 ∈ Mgm ∧ 𝑍𝐵+ Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
13 9 10 11 12 syl3anc ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
14 simpl1 ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → 𝑅 ∈ SRing )
15 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16 15 srgmgp ( 𝑅 ∈ SRing → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
17 mndmgm ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
18 14 16 17 3syl ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
19 15 3 mgpplusg = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
20 19 fneq1i ( Fn ( 𝐵 × 𝐵 ) ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
21 20 biimpi ( Fn ( 𝐵 × 𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
22 21 3ad2ant3 ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
23 22 adantr ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) )
24 15 1 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
25 eqid ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
26 24 25 mgmb1mgm1 ( ( ( mulGrp ‘ 𝑅 ) ∈ Mgm ∧ 𝑍𝐵 ∧ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
27 18 10 23 26 syl3anc ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
28 19 eqcomi ( +g ‘ ( mulGrp ‘ 𝑅 ) ) =
29 28 a1i ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = )
30 29 eqeq1d ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ↔ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
31 27 30 bitrd ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
32 13 31 anbi12d ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( ( 𝐵 = { 𝑍 } ∧ 𝐵 = { 𝑍 } ) ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
33 4 32 syl5bb ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )