Metamath Proof Explorer

Theorem ig1peu

Description: There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1peu.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ig1peu.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
ig1peu.z ⊢ 0 = ( 0g ‘ 𝑃 )
ig1peu.m ⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
ig1peu.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
Assertion ig1peu ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃! 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 ig1peu.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ig1peu.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3 ig1peu.z ⊢ 0 = ( 0g ‘ 𝑃 )
4 ig1peu.m ⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
5 ig1peu.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7 6 2 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
9 8 ssdifd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐼 ∖ { 0 } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) )
10 imass2 ⊢ ( ( 𝐼 ∖ { 0 } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( 𝐷 “ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) ) )
11 9 10 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( 𝐷 “ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) ) )
12 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
13 12 3ad2ant1 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝑅 ∈ Ring )
14 5 1 3 6 deg1n0ima ⊢ ( 𝑅 ∈ Ring → ( 𝐷 “ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) ) ⊆ ℕ0 )
15 13 14 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( ( Base ‘ 𝑃 ) ∖ { 0 } ) ) ⊆ ℕ0 )
16 11 15 sstrd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ℕ0 )
17 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18 16 17 sseqtrdi ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ≥ ‘ 0 ) )
19 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
20 13 19 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝑃 ∈ Ring )
21 simp2 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ∈ 𝑈 )
22 2 3 lidl0cl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 0 ∈ 𝐼 )
23 20 21 22 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 0 ∈ 𝐼 )
24 23 snssd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → { 0 } ⊆ 𝐼 )
25 simp3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝐼 ≠ { 0 } )
26 25 necomd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → { 0 } ≠ 𝐼 )
27 pssdifn0 ⊢ ( ( { 0 } ⊆ 𝐼 ∧ { 0 } ≠ 𝐼 ) → ( 𝐼 ∖ { 0 } ) ≠ ∅ )
28 24 26 27 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐼 ∖ { 0 } ) ≠ ∅ )
29 5 1 6 deg1xrf ⊢ 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ*
30 ffn ⊢ ( 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* → 𝐷 Fn ( Base ‘ 𝑃 ) )
31 29 30 ax-mp ⊢ 𝐷 Fn ( Base ‘ 𝑃 )
32 31 a1i ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
33 8 ssdifssd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐼 ∖ { 0 } ) ⊆ ( Base ‘ 𝑃 ) )
34 fnimaeq0 ⊢ ( ( 𝐷 Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { 0 } ) ⊆ ( Base ‘ 𝑃 ) ) → ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) = ∅ ↔ ( 𝐼 ∖ { 0 } ) = ∅ ) )
35 32 33 34 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) = ∅ ↔ ( 𝐼 ∖ { 0 } ) = ∅ ) )
36 35 necon3bid ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ ↔ ( 𝐼 ∖ { 0 } ) ≠ ∅ ) )
37 28 36 mpbird ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ )
38 infssuzcl ⊢ ( ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ≥ ‘ 0 ) ∧ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ≠ ∅ ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
39 18 37 38 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
40 32 33 fvelimabd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ↔ ∃ ℎ ∈ ( 𝐼 ∖ { 0 } ) ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
41 39 40 mpbid ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃ ℎ ∈ ( 𝐼 ∖ { 0 } ) ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
42 20 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑃 ∈ Ring )
43 simpl2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → 𝐼 ∈ 𝑈 )
44 13 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
45 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
46 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
47 1 45 46 6 ply1sclf ⊢ ( 𝑅 ∈ Ring → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
48 44 47 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
49 simpl1 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → 𝑅 ∈ DivRing )
50 33 sselda ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ℎ ∈ ( Base ‘ 𝑃 ) )
51 eldifsni ⊢ ( ℎ ∈ ( 𝐼 ∖ { 0 } ) → ℎ ≠ 0 )
52 51 adantl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ℎ ≠ 0 )
53 eqid ⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
54 1 6 3 53 drnguc1p ⊢ ( ( 𝑅 ∈ DivRing ∧ ℎ ∈ ( Base ‘ 𝑃 ) ∧ ℎ ≠ 0 ) → ℎ ∈ ( Unic1p ‘ 𝑅 ) )
55 49 50 52 54 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ℎ ∈ ( Unic1p ‘ 𝑅 ) )
56 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
57 5 56 53 uc1pldg ⊢ ( ℎ ∈ ( Unic1p ‘ 𝑅 ) → ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ∈ ( Unit ‘ 𝑅 ) )
58 55 57 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ∈ ( Unit ‘ 𝑅 ) )
59 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
60 56 59 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( Unit ‘ 𝑅 ) )
61 44 58 60 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( Unit ‘ 𝑅 ) )
62 46 56 unitcl ⊢ ( ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( Unit ‘ 𝑅 ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( Base ‘ 𝑅 ) )
63 61 62 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( Base ‘ 𝑅 ) )
64 48 63 ffvelrnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
65 eldifi ⊢ ( ℎ ∈ ( 𝐼 ∖ { 0 } ) → ℎ ∈ 𝐼 )
66 65 adantl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ℎ ∈ 𝐼 )
67 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
68 2 6 67 lidlmcl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ∈ ( Base ‘ 𝑃 ) ∧ ℎ ∈ 𝐼 ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ 𝐼 )
69 42 43 64 66 68 syl22anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ 𝐼 )
70 53 4 1 67 45 5 59 uc1pmon1p ⊢ ( ( 𝑅 ∈ Ring ∧ ℎ ∈ ( Unic1p ‘ 𝑅 ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ 𝑀 )
71 44 55 70 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ 𝑀 )
72 69 71 elind ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ ( 𝐼 ∩ 𝑀 ) )
73 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
74 73 56 unitrrg ⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
75 44 74 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
76 75 61 sseldd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( RLReg ‘ 𝑅 ) )
77 5 1 73 6 67 45 deg1mul3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ∈ ( RLReg ‘ 𝑅 ) ∧ ℎ ∈ ( Base ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ) = ( 𝐷 ‘ ℎ ) )
78 44 76 50 77 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐷 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ) = ( 𝐷 ‘ ℎ ) )
79 fveqeq2 ⊢ ( 𝑔 = ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) → ( ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ℎ ) ↔ ( 𝐷 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ) = ( 𝐷 ‘ ℎ ) ) )
80 79 rspcev ⊢ ( ( ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ∈ ( 𝐼 ∩ 𝑀 ) ∧ ( 𝐷 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ ( ( invr ‘ 𝑅 ) ‘ ( ( coe1 ‘ ℎ ) ‘ ( 𝐷 ‘ ℎ ) ) ) ) ( .r ‘ 𝑃 ) ℎ ) ) = ( 𝐷 ‘ ℎ ) ) → ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ℎ ) )
81 72 78 80 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ℎ ) )
82 eqeq2 ⊢ ( ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ( ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ℎ ) ↔ ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
83 82 rexbidv ⊢ ( ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ( ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ ℎ ) ↔ ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
84 81 83 syl5ibcom ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ℎ ∈ ( 𝐼 ∖ { 0 } ) ) → ( ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
85 84 rexlimdva ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( ∃ ℎ ∈ ( 𝐼 ∖ { 0 } ) ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
86 41 85 mpd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
87 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
88 13 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → 𝑅 ∈ Ring )
89 simprl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) )
90 89 elin2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑔 ∈ 𝑀 )
91 90 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → 𝑔 ∈ 𝑀 )
92 simprl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
93 simprr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ℎ ∈ ( 𝐼 ∩ 𝑀 ) )
94 93 elin2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ℎ ∈ 𝑀 )
95 94 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → ℎ ∈ 𝑀 )
96 simprr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
97 5 4 1 87 88 91 92 95 96 deg1submon1p ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) < inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
98 97 ex ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) < inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
99 18 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ≥ ‘ 0 ) )
100 31 a1i ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
101 33 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝐼 ∖ { 0 } ) ⊆ ( Base ‘ 𝑃 ) )
102 20 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑃 ∈ Ring )
103 simpl2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝐼 ∈ 𝑈 )
104 89 elin1d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑔 ∈ 𝐼 )
105 93 elin1d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ℎ ∈ 𝐼 )
106 2 87 lidlsubcl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ℎ ∈ 𝐼 ) ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ 𝐼 )
107 102 103 104 105 106 syl22anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ 𝐼 )
108 107 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ 𝐼 )
109 simpr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 )
110 eldifsn ⊢ ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( 𝐼 ∖ { 0 } ) ↔ ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ 𝐼 ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) )
111 108 109 110 sylanbrc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( 𝐼 ∖ { 0 } ) )
112 fnfvima ⊢ ( ( 𝐷 Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { 0 } ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( 𝐼 ∖ { 0 } ) ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
113 100 101 111 112 syl3anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
114 infssuzle ⊢ ( ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ( ℤ≥ ‘ 0 ) ∧ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ∈ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) )
115 99 113 114 syl2anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) ∧ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) )
116 115 ex ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ) )
117 imassrn ⊢ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ran 𝐷
118 frn ⊢ ( 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* → ran 𝐷 ⊆ ℝ* )
119 29 118 ax-mp ⊢ ran 𝐷 ⊆ ℝ*
120 117 119 sstri ⊢ ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) ⊆ ℝ*
121 120 39 sselid ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∈ ℝ* )
122 121 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∈ ℝ* )
123 ringgrp ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
124 20 123 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → 𝑃 ∈ Grp )
125 124 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑃 ∈ Grp )
126 inss1 ⊢ ( 𝐼 ∩ 𝑀 ) ⊆ 𝐼
127 126 8 sstrid ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ( 𝐼 ∩ 𝑀 ) ⊆ ( Base ‘ 𝑃 ) )
128 127 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( 𝐼 ∩ 𝑀 ) ⊆ ( Base ‘ 𝑃 ) )
129 128 89 sseldd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → 𝑔 ∈ ( Base ‘ 𝑃 ) )
130 128 93 sseldd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ℎ ∈ ( Base ‘ 𝑃 ) )
131 6 87 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑔 ∈ ( Base ‘ 𝑃 ) ∧ ℎ ∈ ( Base ‘ 𝑃 ) ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( Base ‘ 𝑃 ) )
132 125 129 130 131 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( Base ‘ 𝑃 ) )
133 5 1 6 deg1xrcl ⊢ ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ∈ ℝ* )
134 132 133 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ∈ ℝ* )
135 122 134 xrlenltd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ≤ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) ↔ ¬ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) < inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
136 116 135 sylibd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ≠ 0 → ¬ ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) < inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
137 136 necon4ad ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( 𝐷 ‘ ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) ) < inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) = 0 ) )
138 98 137 syld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) → ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) = 0 ) )
139 6 3 87 grpsubeq0 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑔 ∈ ( Base ‘ 𝑃 ) ∧ ℎ ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) = 0 ↔ 𝑔 = ℎ ) )
140 125 129 130 139 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( 𝑔 ( -g ‘ 𝑃 ) ℎ ) = 0 ↔ 𝑔 = ℎ ) )
141 138 140 sylibd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) ∧ ( 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∧ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ) ) → ( ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) → 𝑔 = ℎ ) )
142 141 ralrimivva ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∀ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∀ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ( ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) → 𝑔 = ℎ ) )
143 fveqeq2 ⊢ ( 𝑔 = ℎ → ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ↔ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
144 143 reu4 ⊢ ( ∃! 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ↔ ( ∃ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ∀ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ∀ ℎ ∈ ( 𝐼 ∩ 𝑀 ) ( ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ∧ ( 𝐷 ‘ ℎ ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) → 𝑔 = ℎ ) ) )
145 86 142 144 sylanbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝐼 ≠ { 0 } ) → ∃! 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )