Metamath Proof Explorer

Theorem zlidlring

Description: The zero (left) ideal of a non-unital ring is a unital ring (the zero ring). (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
zlidlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
zlidlring.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion zlidlring ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝐼 ∈ Ring )

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 zlidlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 zlidlring.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 1 4 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝐿 )
6 5 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → { 0 } ∈ 𝐿 )
7 eleq1 ⊢ ( 𝑈 = { 0 } → ( 𝑈 ∈ 𝐿 ↔ { 0 } ∈ 𝐿 ) )
8 7 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ( 𝑈 ∈ 𝐿 ↔ { 0 } ∈ 𝐿 ) )
9 6 8 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝑈 ∈ 𝐿 )
10 1 2 lidlrng ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )
11 9 10 syldan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝐼 ∈ Rng )
12 eleq1 ⊢ ( { 0 } = 𝑈 → ( { 0 } ∈ 𝐿 ↔ 𝑈 ∈ 𝐿 ) )
13 12 eqcoms ⊢ ( 𝑈 = { 0 } → ( { 0 } ∈ 𝐿 ↔ 𝑈 ∈ 𝐿 ) )
14 13 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ( { 0 } ∈ 𝐿 ↔ 𝑈 ∈ 𝐿 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 15 4 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 15 17 4 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
19 18 18 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) )
20 16 19 mpdan ⊢ ( 𝑅 ∈ Ring → ( ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) )
21 4 fvexi ⊢ 0 ∈ V
22 oveq2 ⊢ ( 𝑦 = 0 → ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0 ( .r ‘ 𝑅 ) 0 ) )
23 id ⊢ ( 𝑦 = 0 → 𝑦 = 0 )
24 22 23 eqeq12d ⊢ ( 𝑦 = 0 → ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ↔ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) )
25 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = ( 0 ( .r ‘ 𝑅 ) 0 ) )
26 25 23 eqeq12d ⊢ ( 𝑦 = 0 → ( ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ↔ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) )
27 24 26 anbi12d ⊢ ( 𝑦 = 0 → ( ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ↔ ( ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) ) )
28 27 ralsng ⊢ ( 0 ∈ V → ( ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ↔ ( ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) ) )
29 21 28 mp1i ⊢ ( 𝑅 ∈ Ring → ( ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ↔ ( ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) ) )
30 20 29 mpbird ⊢ ( 𝑅 ∈ Ring → ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) )
31 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0 ( .r ‘ 𝑅 ) 𝑦 ) )
32 31 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ↔ ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ) )
33 32 ovanraleqv ⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ) )
34 33 rexsng ⊢ ( 0 ∈ V → ( ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ) )
35 21 34 mp1i ⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 0 } ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 0 ) = 𝑦 ) ) )
36 30 35 mpbird ⊢ ( 𝑅 ∈ Ring → ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
37 36 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
38 37 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
39 1 2 lidlbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )
40 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝑈 = { 0 } )
41 39 40 sylan9eqr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( Base ‘ 𝐼 ) = { 0 } )
42 2 17 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
43 42 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
44 43 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
45 44 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
46 45 eqeq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ) )
47 44 oveqd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
48 47 eqeq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
49 46 48 anbi12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
50 41 49 raleqbidv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
51 41 50 rexeqbidv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ { 0 } ∀ 𝑦 ∈ { 0 } ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
52 38 51 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) ∧ 𝑈 ∈ 𝐿 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) )
53 52 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ( 𝑈 ∈ 𝐿 → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
54 14 53 sylbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ( { 0 } ∈ 𝐿 → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
55 6 54 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) )
56 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
57 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
58 56 57 isringrng ⊢ ( 𝐼 ∈ Ring ↔ ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
59 11 55 58 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝐼 ∈ Ring )