Metamath Proof Explorer

Theorem lidlrng

Description: A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020)

Ref Expression
Hypotheses lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
Assertion lidlrng ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 1 2 lidlabl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Abel )
4 1 2 lidlmsgrp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( mulGrp ‘ 𝐼 ) ∈ Smgrp )
5 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → 𝑅 ∈ Ring )
6 1 2 lidlssbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ⊆ ( Base ‘ 𝑅 ) )
7 6 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ∈ ( Base ‘ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
8 6 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ∈ ( Base ‘ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
9 6 sseld ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑐 ∈ ( Base ‘ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
10 7 8 9 3anim123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
11 10 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
12 11 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 13 14 15 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
17 5 12 16 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
18 13 14 15 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
19 5 12 18 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
20 17 19 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐼 ) ∧ 𝑏 ∈ ( Base ‘ 𝐼 ) ∧ 𝑐 ∈ ( Base ‘ 𝐼 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
21 20 ralrimivvva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
22 2 15 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
23 22 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
24 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑎 = 𝑎 )
25 2 14 ressplusg ⊢ ( 𝑈 ∈ 𝐿 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐼 ) )
26 25 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( +g ‘ 𝐼 ) = ( +g ‘ 𝑅 ) )
27 26 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) )
28 23 24 27 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) )
29 23 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) )
30 23 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) )
31 26 29 30 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) )
32 28 31 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
33 26 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) )
34 eqidd ⊢ ( 𝑈 ∈ 𝐿 → 𝑐 = 𝑐 )
35 23 33 34 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) )
36 23 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) = ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) )
37 26 30 36 oveq123d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) )
38 35 37 eqeq12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ↔ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) )
39 32 38 anbi12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
40 39 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
41 40 ralbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
42 41 2ralbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑐 ) ) ) ) )
43 21 42 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) )
44 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
45 eqid ⊢ ( mulGrp ‘ 𝐼 ) = ( mulGrp ‘ 𝐼 )
46 eqid ⊢ ( +g ‘ 𝐼 ) = ( +g ‘ 𝐼 )
47 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
48 44 45 46 47 isrng ⊢ ( 𝐼 ∈ Rng ↔ ( 𝐼 ∈ Abel ∧ ( mulGrp ‘ 𝐼 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐼 ) ∀ 𝑏 ∈ ( Base ‘ 𝐼 ) ∀ 𝑐 ∈ ( Base ‘ 𝐼 ) ( ( 𝑎 ( .r ‘ 𝐼 ) ( 𝑏 ( +g ‘ 𝐼 ) 𝑐 ) ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑏 ) ( +g ‘ 𝐼 ) ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐼 ) 𝑏 ) ( .r ‘ 𝐼 ) 𝑐 ) = ( ( 𝑎 ( .r ‘ 𝐼 ) 𝑐 ) ( +g ‘ 𝐼 ) ( 𝑏 ( .r ‘ 𝐼 ) 𝑐 ) ) ) ) )
49 3 4 43 48 syl3anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )