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 ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )