Metamath Proof Explorer

Theorem edompidlem

Description: Lemma for edompid : In a Euclidean domain, all (non-zero) ideals are generated by a single element. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses edompidlem.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
edompidlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
edompidlem.k ⊢ 𝐾 = ( RSpan ‘ 𝐷 )
edompidlem.e ⊢ 𝐸 = ( EuclF ‘ 𝐷 )
edompidlem.m ⊢ 𝑀 = inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < )
edompidlem.d ⊢ ( 𝜑 → 𝐷 ∈ EDomn )
edompidlem.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝐷 ) )
edompidlem.1 ⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
Assertion edompidlem ( 𝜑 → ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )

Proof

Step Hyp Ref Expression
1 edompidlem.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 edompidlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
3 edompidlem.k ⊢ 𝐾 = ( RSpan ‘ 𝐷 )
4 edompidlem.e ⊢ 𝐸 = ( EuclF ‘ 𝐷 )
5 edompidlem.m ⊢ 𝑀 = inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < )
6 edompidlem.d ⊢ ( 𝜑 → 𝐷 ∈ EDomn )
7 edompidlem.i ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝐷 ) )
8 edompidlem.1 ⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
9 eqid ⊢ ( LIdeal ‘ 𝐷 ) = ( LIdeal ‘ 𝐷 )
10 1 9 lidlss ⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝐷 ) → 𝐼 ⊆ 𝐵 )
11 7 10 syl ⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
12 11 ssdifssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 0 } ) ⊆ 𝐵 )
13 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) )
14 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) ∧ 𝑟 = 0 ) → 𝑟 = 0 )
15 ltrel ⊢ Rel <
16 15 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → Rel < )
17 ltwenn0 ⊢ < We ℕ0
18 17 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → < We ℕ0 )
19 4 fvexi ⊢ 𝐸 ∈ V
20 19 a1i ⊢ ( 𝜑 → 𝐸 ∈ V )
21 20 imaexd ⊢ ( 𝜑 → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ∈ V )
22 21 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ∈ V )
23 11 ssdifd ⊢ ( 𝜑 → ( 𝐼 ∖ { 0 } ) ⊆ ( 𝐵 ∖ { 0 } ) )
24 imass2 ⊢ ( ( 𝐼 ∖ { 0 } ) ⊆ ( 𝐵 ∖ { 0 } ) → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( 𝐸 “ ( 𝐵 ∖ { 0 } ) ) )
25 23 24 syl ⊢ ( 𝜑 → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( 𝐸 “ ( 𝐵 ∖ { 0 } ) ) )
26 resima ⊢ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐵 ∖ { 0 } ) ) = ( 𝐸 “ ( 𝐵 ∖ { 0 } ) )
27 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
28 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
29 4 reseq1i ⊢ ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) )
30 1 2 27 28 29 isedom ⊢ ( 𝐷 ∈ EDomn ↔ ( 𝐷 ∈ IDomn ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
31 6 30 sylib ⊢ ( 𝜑 → ( 𝐷 ∈ IDomn ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
32 31 simprld ⊢ ( 𝜑 → ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 )
33 32 fimassd ⊢ ( 𝜑 → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 )
34 26 33 eqsstrrid ⊢ ( 𝜑 → ( 𝐸 “ ( 𝐵 ∖ { 0 } ) ) ⊆ ℕ0 )
35 25 34 sstrd ⊢ ( 𝜑 → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ℕ0 )
36 35 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ℕ0 )
37 31 simpld ⊢ ( 𝜑 → 𝐷 ∈ IDomn )
38 37 idomringd ⊢ ( 𝜑 → 𝐷 ∈ Ring )
39 9 2 lidl0cl ⊢ ( ( 𝐷 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝐷 ) ) → 0 ∈ 𝐼 )
40 38 7 39 syl2anc ⊢ ( 𝜑 → 0 ∈ 𝐼 )
41 40 snssd ⊢ ( 𝜑 → { 0 } ⊆ 𝐼 )
42 8 necomd ⊢ ( 𝜑 → { 0 } ≠ 𝐼 )
43 pssdifn0 ⊢ ( ( { 0 } ⊆ 𝐼 ∧ { 0 } ≠ 𝐼 ) → ( 𝐼 ∖ { 0 } ) ≠ ∅ )
44 41 42 43 syl2anc ⊢ ( 𝜑 → ( 𝐼 ∖ { 0 } ) ≠ ∅ )
45 32 ffnd ⊢ ( 𝜑 → ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) )
47 23 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝐼 ∖ { 0 } ) )
49 46 47 48 fnfvimad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) ∈ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) )
50 resima2 ⊢ ( ( 𝐼 ∖ { 0 } ) ⊆ ( 𝐵 ∖ { 0 } ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) = ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
51 23 50 syl ⊢ ( 𝜑 → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) = ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) = ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
53 49 52 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑥 ) ∈ ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
54 53 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ )
55 44 54 n0limd ⊢ ( 𝜑 → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ )
56 55 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ )
57 45 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) Fn ( 𝐵 ∖ { 0 } ) )
58 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐵 )
59 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
60 58 59 eldifsnd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ( 𝐵 ∖ { 0 } ) )
61 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) )
62 61 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑎 ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) = ( ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) )
63 38 ringabld ⊢ ( 𝜑 → 𝐷 ∈ Abel )
64 63 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝐷 ∈ Abel )
65 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝐷 ∈ Ring )
66 65 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝐷 ∈ Ring )
67 23 sselda ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑔 ∈ ( 𝐵 ∖ { 0 } ) )
68 67 eldifad ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑔 ∈ 𝐵 )
69 68 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑔 ∈ 𝐵 )
70 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑞 ∈ 𝐵 )
71 1 28 66 69 70 ringcld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ∈ 𝐵 )
72 eqid ⊢ ( -g ‘ 𝐷 ) = ( -g ‘ 𝐷 )
73 1 27 72 ablpncan2 ⊢ ( ( 𝐷 ∈ Abel ∧ ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) = 𝑟 )
74 64 71 58 73 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) = 𝑟 )
75 62 74 eqtr2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 = ( 𝑎 ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) )
76 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝐼 ∈ ( LIdeal ‘ 𝐷 ) )
77 76 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝐼 ∈ ( LIdeal ‘ 𝐷 ) )
78 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑎 ∈ 𝐼 )
79 37 idomcringd ⊢ ( 𝜑 → 𝐷 ∈ CRing )
80 79 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) → 𝐷 ∈ CRing )
81 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) → 𝑞 ∈ 𝐵 )
82 68 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) → 𝑔 ∈ 𝐵 )
83 1 28 80 81 82 crngcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) → ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) = ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) )
84 83 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) = ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) )
85 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝑔 ∈ ( 𝐼 ∖ { 0 } ) )
86 85 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝑔 ∈ 𝐼 )
87 86 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑔 ∈ 𝐼 )
88 9 1 28 66 77 70 87 lidlmcld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) ∈ 𝐼 )
89 84 88 eqeltrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ∈ 𝐼 )
90 9 72 lidlsubcl ⊢ ( ( ( 𝐷 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ∈ 𝐼 ) ) → ( 𝑎 ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) ∈ 𝐼 )
91 66 77 78 89 90 syl22anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝑎 ( -g ‘ 𝐷 ) ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ) ∈ 𝐼 )
92 75 91 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐼 )
93 92 59 eldifsnd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ( 𝐼 ∖ { 0 } ) )
94 57 60 93 fnfvimad ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) ∈ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) )
95 60 fvresd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) = ( 𝐸 ‘ 𝑟 ) )
96 51 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) = ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
97 94 95 96 3eltr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( 𝐸 ‘ 𝑟 ) ∈ ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
98 16 18 22 36 56 97 weinflb ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ¬ ( 𝐸 ‘ 𝑟 ) < inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < ) )
99 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 )
100 67 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑔 ∈ ( 𝐵 ∖ { 0 } ) )
101 100 fvresd ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = ( 𝐸 ‘ 𝑔 ) )
102 101 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = ( 𝐸 ‘ 𝑔 ) )
103 5 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑀 = inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < ) )
104 99 102 103 3eqtr3rd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < ) = ( 𝐸 ‘ 𝑔 ) )
105 98 104 brneqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ¬ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) )
106 105 ex ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) → ( 𝑟 ≠ 0 → ¬ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) )
107 106 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝑟 ≠ 0 → ¬ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) )
108 107 necon4ad ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) → 𝑟 = 0 ) )
109 108 imp ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) ∧ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) → 𝑟 = 0 )
110 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) )
111 14 109 110 mpjaodan ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑟 = 0 )
112 111 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 0 ) )
113 38 ringgrpd ⊢ ( 𝜑 → 𝐷 ∈ Grp )
114 113 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝐷 ∈ Grp )
115 65 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝐷 ∈ Ring )
116 68 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑔 ∈ 𝐵 )
117 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑞 ∈ 𝐵 )
118 1 28 115 116 117 ringcld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ∈ 𝐵 )
119 1 27 2 114 118 grpridd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 0 ) = ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) )
120 13 112 119 3eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑎 = ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) )
121 83 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) = ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) )
122 120 121 eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑎 = ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) )
123 38 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝐷 ∈ Ring )
124 68 snssd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → { 𝑔 } ⊆ 𝐵 )
125 3 1 9 rspcl ⊢ ( ( 𝐷 ∈ Ring ∧ { 𝑔 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝐷 ) )
126 123 124 125 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝐷 ) )
127 126 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝐷 ) )
128 1 3 rspsnid ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
129 123 68 128 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
130 129 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
131 9 1 28 115 127 117 130 lidlmcld ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → ( 𝑞 ( .r ‘ 𝐷 ) 𝑔 ) ∈ ( 𝐾 ‘ { 𝑔 } ) )
132 122 131 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) → 𝑎 ∈ ( 𝐾 ‘ { 𝑔 } ) )
133 132 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ ( 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) ) → 𝑎 ∈ ( 𝐾 ‘ { 𝑔 } ) )
134 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → 𝐷 ∈ EDomn )
135 76 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝐼 ⊆ 𝐵 )
136 135 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ 𝐵 )
137 1 2 27 28 4 134 136 100 edomediv ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑎 = ( ( 𝑔 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑔 ) ) ) )
138 133 137 r19.29vva ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ ( 𝐾 ‘ { 𝑔 } ) )
139 138 ex ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → ( 𝑎 ∈ 𝐼 → 𝑎 ∈ ( 𝐾 ‘ { 𝑔 } ) ) )
140 139 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝐼 ⊆ ( 𝐾 ‘ { 𝑔 } ) )
141 86 snssd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → { 𝑔 } ⊆ 𝐼 )
142 3 9 rspssp ⊢ ( ( 𝐷 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝐷 ) ∧ { 𝑔 } ⊆ 𝐼 ) → ( 𝐾 ‘ { 𝑔 } ) ⊆ 𝐼 )
143 65 76 141 142 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → ( 𝐾 ‘ { 𝑔 } ) ⊆ 𝐼 )
144 140 143 eqssd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ) ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 ) → 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )
145 nfcv ⊢ Ⅎ 𝑔 ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) )
146 17 a1i ⊢ ( 𝜑 → < We ℕ0 )
147 146 21 35 55 weinfcl ⊢ ( 𝜑 → inf ( ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) , ℕ0 , < ) ∈ ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
148 5 147 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐸 “ ( 𝐼 ∖ { 0 } ) ) )
149 148 51 eleqtrrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) “ ( 𝐼 ∖ { 0 } ) ) )
150 145 45 149 fvelimad ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( ( 𝐵 ∖ { 0 } ) ∩ ( 𝐼 ∖ { 0 } ) ) ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 )
151 sseqin2 ⊢ ( ( 𝐼 ∖ { 0 } ) ⊆ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝐵 ∖ { 0 } ) ∩ ( 𝐼 ∖ { 0 } ) ) = ( 𝐼 ∖ { 0 } ) )
152 23 151 sylib ⊢ ( 𝜑 → ( ( 𝐵 ∖ { 0 } ) ∩ ( 𝐼 ∖ { 0 } ) ) = ( 𝐼 ∖ { 0 } ) )
153 150 152 rexeqtrdv ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑔 ) = 𝑀 )
154 144 153 reximddv3 ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )
155 ssrexv ⊢ ( ( 𝐼 ∖ { 0 } ) ⊆ 𝐵 → ( ∃ 𝑔 ∈ ( 𝐼 ∖ { 0 } ) 𝐼 = ( 𝐾 ‘ { 𝑔 } ) → ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) ) )
156 12 154 155 sylc ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐵 𝐼 = ( 𝐾 ‘ { 𝑔 } ) )