This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnglidl0

Description: Every non-unital ring contains a zero ideal. (Contributed by AV, 19-Feb-2025)

Ref Expression
Hypotheses rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
rnglidl0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion rnglidl0 ( 𝑅 ∈ Rng → { 0 } ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 rnglidl0.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 2 rng0cl ⊢ ( 𝑅 ∈ Rng → 0 ∈ ( Base ‘ 𝑅 ) )
5 4 snssd ⊢ ( 𝑅 ∈ Rng → { 0 } ⊆ ( Base ‘ 𝑅 ) )
6 2 fvexi ⊢ 0 ∈ V
7 6 a1i ⊢ ( 𝑅 ∈ Rng → 0 ∈ V )
8 7 snn0d ⊢ ( 𝑅 ∈ Rng → { 0 } ≠ ∅ )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 3 9 2 rngrz ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 0 ) = 0 )
11 10 oveq1d ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) = ( 0 ( +g ‘ 𝑅 ) 0 ) )
12 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
13 3 2 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
14 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
15 3 14 2 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
16 12 13 15 syl2anc2 ⊢ ( 𝑅 ∈ Rng → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
17 16 adantr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
18 11 17 eqtrd ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) = 0 )
19 6 elsn2 ⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) ∈ { 0 } ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) = 0 )
20 18 19 sylibr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) ∈ { 0 } )
21 oveq2 ⊢ ( 𝑦 = 0 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 0 ) )
22 21 oveq1d ⊢ ( 𝑦 = 0 → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) )
23 22 eleq1d ⊢ ( 𝑦 = 0 → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ) )
24 23 ralbidv ⊢ ( 𝑦 = 0 → ( ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ) )
25 6 24 ralsn ⊢ ( ∀ 𝑦 ∈ { 0 } ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } )
26 oveq2 ⊢ ( 𝑧 = 0 → ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) )
27 26 eleq1d ⊢ ( 𝑧 = 0 → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) ∈ { 0 } ) )
28 6 27 ralsn ⊢ ( ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) ∈ { 0 } )
29 25 28 bitri ⊢ ( ∀ 𝑦 ∈ { 0 } ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 0 ) ( +g ‘ 𝑅 ) 0 ) ∈ { 0 } )
30 20 29 sylibr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑦 ∈ { 0 } ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } )
31 30 ralrimiva ⊢ ( 𝑅 ∈ Rng → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ { 0 } ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } )
32 1 3 14 9 islidl ⊢ ( { 0 } ∈ 𝑈 ↔ ( { 0 } ⊆ ( Base ‘ 𝑅 ) ∧ { 0 } ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ { 0 } ∀ 𝑧 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) ∈ { 0 } ) )
33 5 8 31 32 syl3anbrc ⊢ ( 𝑅 ∈ Rng → { 0 } ∈ 𝑈 )