This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( ( 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 ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ∥ 𝑋 )