Metamath Proof Explorer

Theorem uzlidlring

Description: Only the zero (left) ideal or the unit (left) ideal of a domain is a unital ring. (Contributed by AV, 18-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 lidlabl.l ⊢ 𝐿 = ( LIdeal ‘ 𝑅 )
2 lidlabl.i ⊢ 𝐼 = ( 𝑅 ↾s 𝑈 )
3 zlidlring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 zlidlring.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
6 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
7 5 6 isringrng ⊢ ( 𝐼 ∈ Ring ↔ ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
8 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
9 8 anim1i ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) )
10 1 2 lidlrng ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )
11 9 10 syl ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) → 𝐼 ∈ Rng )
12 ibar ⊢ ( 𝐼 ∈ Rng → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) ) )
13 12 bicomd ⊢ ( 𝐼 ∈ Rng → ( ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
14 13 adantl ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 2 15 ressmulr ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐼 ) )
17 16 eqcomd ⊢ ( 𝑈 ∈ 𝐿 → ( .r ‘ 𝐼 ) = ( .r ‘ 𝑅 ) )
18 17 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
19 18 eqeq1d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ) )
20 17 oveqd ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
21 20 eqeq1d ⊢ ( 𝑈 ∈ 𝐿 → ( ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
22 19 21 anbi12d ⊢ ( 𝑈 ∈ 𝐿 → ( ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
23 22 ad2antlr ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
24 23 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
25 24 ralbidv ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
26 simp-4l ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → 𝑅 ∈ Domn )
27 1 2 lidlbas ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) = 𝑈 )
28 27 eleq1d ⊢ ( 𝑈 ∈ 𝐿 → ( ( Base ‘ 𝐼 ) ∈ 𝐿 ↔ 𝑈 ∈ 𝐿 ) )
29 28 ibir ⊢ ( 𝑈 ∈ 𝐿 → ( Base ‘ 𝐼 ) ∈ 𝐿 )
30 29 ad3antlr ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( Base ‘ 𝐼 ) ∈ 𝐿 )
31 27 ad2antlr ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( Base ‘ 𝐼 ) = 𝑈 )
32 31 eqeq1d ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( Base ‘ 𝐼 ) = { 0 } ↔ 𝑈 = { 0 } ) )
33 32 biimpd ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( Base ‘ 𝐼 ) = { 0 } → 𝑈 = { 0 } ) )
34 33 necon3bd ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ¬ 𝑈 = { 0 } → ( Base ‘ 𝐼 ) ≠ { 0 } ) )
35 34 imp ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( Base ‘ 𝐼 ) ≠ { 0 } )
36 30 35 jca ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( ( Base ‘ 𝐼 ) ∈ 𝐿 ∧ ( Base ‘ 𝐼 ) ≠ { 0 } ) )
37 36 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ( Base ‘ 𝐼 ) ∈ 𝐿 ∧ ( Base ‘ 𝐼 ) ≠ { 0 } ) )
38 simpr ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → 𝑥 ∈ ( Base ‘ 𝐼 ) )
39 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
40 1 15 39 4 lidldomn1 ⊢ ( ( 𝑅 ∈ Domn ∧ ( ( Base ‘ 𝐼 ) ∈ 𝐿 ∧ ( Base ‘ 𝐼 ) ≠ { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) → 𝑥 = ( 1r ‘ 𝑅 ) ) )
41 26 37 38 40 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) → 𝑥 = ( 1r ‘ 𝑅 ) ) )
42 25 41 sylbid ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) → 𝑥 = ( 1r ‘ 𝑅 ) ) )
43 42 imp ⊢ ( ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → 𝑥 = ( 1r ‘ 𝑅 ) )
44 27 ad3antlr ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( Base ‘ 𝐼 ) = 𝑈 )
45 44 eleq2d ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( 𝑥 ∈ ( Base ‘ 𝐼 ) ↔ 𝑥 ∈ 𝑈 ) )
46 45 biimpd ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( 𝑥 ∈ ( Base ‘ 𝐼 ) → 𝑥 ∈ 𝑈 ) )
47 46 imp ⊢ ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) → 𝑥 ∈ 𝑈 )
48 47 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → 𝑥 ∈ 𝑈 )
49 43 48 eqeltrrd ⊢ ( ( ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) ∧ 𝑥 ∈ ( Base ‘ 𝐼 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
50 49 rexlimdva2 ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ¬ 𝑈 = { 0 } ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 ) )
51 50 impancom ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → ( ¬ 𝑈 = { 0 } → ( 1r ‘ 𝑅 ) ∈ 𝑈 ) )
52 9 adantr ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) )
53 1 3 39 lidl1el ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑈 ↔ 𝑈 = 𝐵 ) )
54 52 53 syl ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑈 ↔ 𝑈 = 𝐵 ) )
55 54 adantr ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑈 ↔ 𝑈 = 𝐵 ) )
56 51 55 sylibd ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → ( ¬ 𝑈 = { 0 } → 𝑈 = 𝐵 ) )
57 56 orrd ⊢ ( ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) → ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) )
58 57 ex ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) → ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )
59 1 2 3 4 zlidlring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → 𝐼 ∈ Ring )
60 7 simprbi ⊢ ( 𝐼 ∈ Ring → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) )
61 59 60 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 = { 0 } ) → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) )
62 61 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑈 = { 0 } → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
63 8 62 syl ⊢ ( 𝑅 ∈ Domn → ( 𝑈 = { 0 } → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
64 63 ad2antrr ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( 𝑈 = { 0 } → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
65 9 anim1i ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) )
66 3 15 ringideu ⊢ ( 𝑅 ∈ Ring → ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
67 reurex ⊢ ( ∃! 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
68 66 67 syl ⊢ ( 𝑅 ∈ Ring → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
69 68 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
70 69 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) )
71 2 3 ressbas ⊢ ( 𝑈 ∈ 𝐿 → ( 𝑈 ∩ 𝐵 ) = ( Base ‘ 𝐼 ) )
72 71 ad3antlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( 𝑈 ∩ 𝐵 ) = ( Base ‘ 𝐼 ) )
73 ineq1 ⊢ ( 𝑈 = 𝐵 → ( 𝑈 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐵 ) )
74 inidm ⊢ ( 𝐵 ∩ 𝐵 ) = 𝐵
75 73 74 eqtrdi ⊢ ( 𝑈 = 𝐵 → ( 𝑈 ∩ 𝐵 ) = 𝐵 )
76 75 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( 𝑈 ∩ 𝐵 ) = 𝐵 )
77 72 76 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( Base ‘ 𝐼 ) = 𝐵 )
78 22 ad3antlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
79 77 78 raleqbidv ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
80 77 79 rexeqbidv ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
81 70 80 mpbird ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) ∧ 𝑈 = 𝐵 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) )
82 81 ex ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( 𝑈 = 𝐵 → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
83 65 82 syl ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( 𝑈 = 𝐵 → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
84 64 83 jaod ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) → ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) )
85 58 84 impbid ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )
86 14 85 bitrd ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) ∧ 𝐼 ∈ Rng ) → ( ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )
87 11 86 mpdan ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝐼 ∈ Rng ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐼 ) ∀ 𝑦 ∈ ( Base ‘ 𝐼 ) ( ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( .r ‘ 𝐼 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )
88 7 87 syl5bb ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑈 ∈ 𝐿 ) → ( 𝐼 ∈ Ring ↔ ( 𝑈 = { 0 } ∨ 𝑈 = 𝐵 ) ) )