Metamath Proof Explorer


Theorem ig1pdvds

Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

Ref Expression
Hypotheses ig1pval.p 𝑃 = ( Poly1𝑅 )
ig1pval.g 𝐺 = ( idlGen1p𝑅 )
ig1pcl.u 𝑈 = ( LIdeal ‘ 𝑃 )
ig1pdvds.d = ( ∥r𝑃 )
Assertion ig1pdvds ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → ( 𝐺𝐼 ) 𝑋 )

Proof

Step Hyp Ref Expression
1 ig1pval.p 𝑃 = ( Poly1𝑅 )
2 ig1pval.g 𝐺 = ( idlGen1p𝑅 )
3 ig1pcl.u 𝑈 = ( LIdeal ‘ 𝑃 )
4 ig1pdvds.d = ( ∥r𝑃 )
5 drngring ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6 1 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
7 5 6 syl ( 𝑅 ∈ DivRing → 𝑃 ∈ Ring )
8 7 3ad2ant1 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → 𝑃 ∈ Ring )
9 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10 9 3 lidlss ( 𝐼𝑈𝐼 ⊆ ( Base ‘ 𝑃 ) )
11 10 3ad2ant2 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
12 1 2 3 ig1pcl ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈 ) → ( 𝐺𝐼 ) ∈ 𝐼 )
13 12 3adant3 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → ( 𝐺𝐼 ) ∈ 𝐼 )
14 11 13 sseldd ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → ( 𝐺𝐼 ) ∈ ( Base ‘ 𝑃 ) )
15 eqid ( 0g𝑃 ) = ( 0g𝑃 )
16 9 4 15 dvdsr01 ( ( 𝑃 ∈ Ring ∧ ( 𝐺𝐼 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝐺𝐼 ) ( 0g𝑃 ) )
17 8 14 16 syl2anc ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → ( 𝐺𝐼 ) ( 0g𝑃 ) )
18 17 adantr ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 = { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) ( 0g𝑃 ) )
19 eleq2 ( 𝐼 = { ( 0g𝑃 ) } → ( 𝑋𝐼𝑋 ∈ { ( 0g𝑃 ) } ) )
20 19 biimpac ( ( 𝑋𝐼𝐼 = { ( 0g𝑃 ) } ) → 𝑋 ∈ { ( 0g𝑃 ) } )
21 20 3ad2antl3 ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 = { ( 0g𝑃 ) } ) → 𝑋 ∈ { ( 0g𝑃 ) } )
22 elsni ( 𝑋 ∈ { ( 0g𝑃 ) } → 𝑋 = ( 0g𝑃 ) )
23 21 22 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 = { ( 0g𝑃 ) } ) → 𝑋 = ( 0g𝑃 ) )
24 18 23 breqtrrd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 = { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) 𝑋 )
25 simpl1 ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝑅 ∈ DivRing )
26 25 5 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝑅 ∈ Ring )
27 simpl2 ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝐼𝑈 )
28 27 10 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
29 simpl3 ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝑋𝐼 )
30 28 29 sseldd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
31 simpr ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝐼 ≠ { ( 0g𝑃 ) } )
32 eqid ( deg1𝑅 ) = ( deg1𝑅 )
33 eqid ( Monic1p𝑅 ) = ( Monic1p𝑅 )
34 1 2 15 3 32 33 ig1pval3 ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ ( Monic1p𝑅 ) ∧ ( ( deg1𝑅 ) ‘ ( 𝐺𝐼 ) ) = inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ) )
35 25 27 31 34 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( 𝐺𝐼 ) ∈ 𝐼 ∧ ( 𝐺𝐼 ) ∈ ( Monic1p𝑅 ) ∧ ( ( deg1𝑅 ) ‘ ( 𝐺𝐼 ) ) = inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ) )
36 35 simp2d ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) ∈ ( Monic1p𝑅 ) )
37 eqid ( Unic1p𝑅 ) = ( Unic1p𝑅 )
38 37 33 mon1puc1p ( ( 𝑅 ∈ Ring ∧ ( 𝐺𝐼 ) ∈ ( Monic1p𝑅 ) ) → ( 𝐺𝐼 ) ∈ ( Unic1p𝑅 ) )
39 26 36 38 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) ∈ ( Unic1p𝑅 ) )
40 eqid ( rem1p𝑅 ) = ( rem1p𝑅 )
41 40 1 9 37 32 r1pdeglt ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺𝐼 ) ∈ ( Unic1p𝑅 ) ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) < ( ( deg1𝑅 ) ‘ ( 𝐺𝐼 ) ) )
42 26 30 39 41 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) < ( ( deg1𝑅 ) ‘ ( 𝐺𝐼 ) ) )
43 35 simp3d ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) ‘ ( 𝐺𝐼 ) ) = inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) )
44 42 43 breqtrd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) < inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) )
45 32 1 9 deg1xrf ( deg1𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ*
46 35 simp1d ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) ∈ 𝐼 )
47 28 46 sseldd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) ∈ ( Base ‘ 𝑃 ) )
48 eqid ( quot1p𝑅 ) = ( quot1p𝑅 )
49 eqid ( .r𝑃 ) = ( .r𝑃 )
50 eqid ( -g𝑃 ) = ( -g𝑃 )
51 40 1 9 48 49 50 r1pval ( ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺𝐼 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 𝑋 ( -g𝑃 ) ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ) )
52 30 47 51 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 𝑋 ( -g𝑃 ) ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ) )
53 26 6 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → 𝑃 ∈ Ring )
54 48 1 9 37 q1pcl ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺𝐼 ) ∈ ( Unic1p𝑅 ) ) → ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
55 26 30 39 54 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
56 3 9 49 lidlmcl ( ( ( 𝑃 ∈ Ring ∧ 𝐼𝑈 ) ∧ ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺𝐼 ) ∈ 𝐼 ) ) → ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ∈ 𝐼 )
57 53 27 55 46 56 syl22anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ∈ 𝐼 )
58 3 50 lidlsubcl ( ( ( 𝑃 ∈ Ring ∧ 𝐼𝑈 ) ∧ ( 𝑋𝐼 ∧ ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ∈ 𝐼 ) ) → ( 𝑋 ( -g𝑃 ) ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ) ∈ 𝐼 )
59 53 27 29 57 58 syl22anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( -g𝑃 ) ( ( 𝑋 ( quot1p𝑅 ) ( 𝐺𝐼 ) ) ( .r𝑃 ) ( 𝐺𝐼 ) ) ) ∈ 𝐼 )
60 52 59 eqeltrd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ 𝐼 )
61 28 60 sseldd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( Base ‘ 𝑃 ) )
62 ffvelrn ( ( ( deg1𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ* ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ℝ* )
63 45 61 62 sylancr ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ℝ* )
64 28 ssdifd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐼 ∖ { ( 0g𝑃 ) } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) )
65 imass2 ( ( 𝐼 ∖ { ( 0g𝑃 ) } ) ⊆ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ( deg1𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) ) )
66 64 65 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ( deg1𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) ) )
67 32 1 15 9 deg1n0ima ( 𝑅 ∈ Ring → ( ( deg1𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) ) ⊆ ℕ0 )
68 26 67 syl ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) ) ⊆ ℕ0 )
69 nn0uz 0 = ( ℤ ‘ 0 )
70 68 69 sseqtrdi ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( ( Base ‘ 𝑃 ) ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ℤ ‘ 0 ) )
71 66 70 sstrd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ℤ ‘ 0 ) )
72 uzssz ( ℤ ‘ 0 ) ⊆ ℤ
73 zssre ℤ ⊆ ℝ
74 ressxr ℝ ⊆ ℝ*
75 73 74 sstri ℤ ⊆ ℝ*
76 72 75 sstri ( ℤ ‘ 0 ) ⊆ ℝ*
77 71 76 sstrdi ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ℝ* )
78 3 15 lidl0cl ( ( 𝑃 ∈ Ring ∧ 𝐼𝑈 ) → ( 0g𝑃 ) ∈ 𝐼 )
79 53 27 78 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 0g𝑃 ) ∈ 𝐼 )
80 79 snssd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → { ( 0g𝑃 ) } ⊆ 𝐼 )
81 31 necomd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → { ( 0g𝑃 ) } ≠ 𝐼 )
82 pssdifn0 ( ( { ( 0g𝑃 ) } ⊆ 𝐼 ∧ { ( 0g𝑃 ) } ≠ 𝐼 ) → ( 𝐼 ∖ { ( 0g𝑃 ) } ) ≠ ∅ )
83 80 81 82 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐼 ∖ { ( 0g𝑃 ) } ) ≠ ∅ )
84 ffn ( ( deg1𝑅 ) : ( Base ‘ 𝑃 ) ⟶ ℝ* → ( deg1𝑅 ) Fn ( Base ‘ 𝑃 ) )
85 45 84 ax-mp ( deg1𝑅 ) Fn ( Base ‘ 𝑃 )
86 28 ssdifssd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐼 ∖ { ( 0g𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) )
87 fnimaeq0 ( ( ( deg1𝑅 ) Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) ) → ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) = ∅ ↔ ( 𝐼 ∖ { ( 0g𝑃 ) } ) = ∅ ) )
88 85 86 87 sylancr ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) = ∅ ↔ ( 𝐼 ∖ { ( 0g𝑃 ) } ) = ∅ ) )
89 88 necon3bid ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ≠ ∅ ↔ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ≠ ∅ ) )
90 83 89 mpbird ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ≠ ∅ )
91 infssuzcl ( ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ℤ ‘ 0 ) ∧ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ≠ ∅ ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ∈ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) )
92 71 90 91 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ∈ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) )
93 77 92 sseldd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ∈ ℝ* )
94 xrltnle ( ( ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ℝ* ∧ inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ∈ ℝ* ) → ( ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) < inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ↔ ¬ inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ) )
95 63 93 94 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) < inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ↔ ¬ inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ) )
96 44 95 mpbid ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ¬ inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) )
97 71 adantr ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ℤ ‘ 0 ) )
98 60 adantr ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ 𝐼 )
99 simpr ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) )
100 eldifsn ( ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ↔ ( ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ 𝐼 ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) )
101 98 99 100 sylanbrc ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0g𝑃 ) } ) )
102 fnfvima ( ( ( deg1𝑅 ) Fn ( Base ‘ 𝑃 ) ∧ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ∈ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) )
103 85 86 101 102 mp3an2ani ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) )
104 infssuzle ( ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ⊆ ( ℤ ‘ 0 ) ∧ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ∈ ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) )
105 97 103 104 syl2anc ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) ∧ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) )
106 105 ex ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ≠ ( 0g𝑃 ) → inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) ) )
107 106 necon1bd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ¬ inf ( ( ( deg1𝑅 ) “ ( 𝐼 ∖ { ( 0g𝑃 ) } ) ) , ℝ , < ) ≤ ( ( deg1𝑅 ) ‘ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 0g𝑃 ) ) )
108 96 107 mpd ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 0g𝑃 ) )
109 1 4 9 37 15 40 dvdsr1p ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐺𝐼 ) ∈ ( Unic1p𝑅 ) ) → ( ( 𝐺𝐼 ) 𝑋 ↔ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 0g𝑃 ) ) )
110 26 30 39 109 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( ( 𝐺𝐼 ) 𝑋 ↔ ( 𝑋 ( rem1p𝑅 ) ( 𝐺𝐼 ) ) = ( 0g𝑃 ) ) )
111 108 110 mpbird ( ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) ∧ 𝐼 ≠ { ( 0g𝑃 ) } ) → ( 𝐺𝐼 ) 𝑋 )
112 24 111 pm2.61dane ( ( 𝑅 ∈ DivRing ∧ 𝐼𝑈𝑋𝐼 ) → ( 𝐺𝐼 ) 𝑋 )