Metamath Proof Explorer

Theorem hbtlem5

Description: The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
hbtlem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
hbtlem3.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
hbtlem3.ij ⊢ ( 𝜑 → 𝐼 ⊆ 𝐽 )
hbtlem5.e ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑥 ) )
Assertion hbtlem5 ( 𝜑 → 𝐼 = 𝐽 )

Proof

Step Hyp Ref Expression
1 hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 hbtlem3.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
6 hbtlem3.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
7 hbtlem3.ij ⊢ ( 𝜑 → 𝐼 ⊆ 𝐽 )
8 hbtlem5.e ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑥 ) )
9 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10 9 2 lidlss ⊢ ( 𝐽 ∈ 𝑈 → 𝐽 ⊆ ( Base ‘ 𝑃 ) )
11 6 10 syl ⊢ ( 𝜑 → 𝐽 ⊆ ( Base ‘ 𝑃 ) )
12 11 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → 𝑎 ∈ ( Base ‘ 𝑃 ) )
13 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
14 13 1 9 deg1cl ⊢ ( 𝑎 ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
15 12 14 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) )
16 elun ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ { -∞ } ) )
17 nnssnn0 ⊢ ℕ ⊆ ℕ0
18 nn0re ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℕ0 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℝ )
19 arch ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℝ → ∃ 𝑏 ∈ ℕ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
20 18 19 syl ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℕ0 → ∃ 𝑏 ∈ ℕ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
21 ssrexv ⊢ ( ℕ ⊆ ℕ0 → ( ∃ 𝑏 ∈ ℕ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 ) )
22 17 20 21 mpsyl ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℕ0 → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
23 elsni ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ { -∞ } → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = -∞ )
24 0nn0 ⊢ 0 ∈ ℕ0
25 mnflt0 ⊢ -∞ < 0
26 breq2 ⊢ ( 𝑏 = 0 → ( -∞ < 𝑏 ↔ -∞ < 0 ) )
27 26 rspcev ⊢ ( ( 0 ∈ ℕ0 ∧ -∞ < 0 ) → ∃ 𝑏 ∈ ℕ0 -∞ < 𝑏 )
28 24 25 27 mp2an ⊢ ∃ 𝑏 ∈ ℕ0 -∞ < 𝑏
29 breq1 ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = -∞ → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 ↔ -∞ < 𝑏 ) )
30 29 rexbidv ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = -∞ → ( ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 ↔ ∃ 𝑏 ∈ ℕ0 -∞ < 𝑏 ) )
31 28 30 mpbiri ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = -∞ → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
32 23 31 syl ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ { -∞ } → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
33 22 32 jaoi ⊢ ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ℕ0 ∨ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ { -∞ } ) → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
34 16 33 sylbi ⊢ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( ℕ0 ∪ { -∞ } ) → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
35 15 34 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 )
36 breq2 ⊢ ( 𝑐 = 0 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 ) )
37 36 imbi1d ⊢ ( 𝑐 = 0 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 → 𝑎 ∈ 𝐼 ) ) )
38 37 ralbidv ⊢ ( 𝑐 = 0 → ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 → 𝑎 ∈ 𝐼 ) ) )
39 38 imbi2d ⊢ ( 𝑐 = 0 → ( ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ) ↔ ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 → 𝑎 ∈ 𝐼 ) ) ) )
40 breq2 ⊢ ( 𝑐 = 𝑏 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 ) )
41 40 imbi1d ⊢ ( 𝑐 = 𝑏 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) )
42 41 ralbidv ⊢ ( 𝑐 = 𝑏 → ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) )
43 42 imbi2d ⊢ ( 𝑐 = 𝑏 → ( ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ) ↔ ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ) )
44 breq2 ⊢ ( 𝑐 = ( 𝑏 + 1 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) ) )
45 44 imbi1d ⊢ ( 𝑐 = ( 𝑏 + 1 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) → 𝑎 ∈ 𝐼 ) ) )
46 45 ralbidv ⊢ ( 𝑐 = ( 𝑏 + 1 ) → ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) → 𝑎 ∈ 𝐼 ) ) )
47 fveq2 ⊢ ( 𝑎 = 𝑑 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) )
48 47 breq1d ⊢ ( 𝑎 = 𝑑 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) ) )
49 eleq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 ∈ 𝐼 ↔ 𝑑 ∈ 𝐼 ) )
50 48 49 imbi12d ⊢ ( 𝑎 = 𝑑 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) → 𝑎 ∈ 𝐼 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) ) )
51 50 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < ( 𝑏 + 1 ) → 𝑎 ∈ 𝐼 ) ↔ ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) )
52 46 51 bitrdi ⊢ ( 𝑐 = ( 𝑏 + 1 ) → ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ↔ ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) ) )
53 52 imbi2d ⊢ ( 𝑐 = ( 𝑏 + 1 ) → ( ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑐 → 𝑎 ∈ 𝐼 ) ) ↔ ( 𝜑 → ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) ) ) )
54 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → 𝑅 ∈ Ring )
55 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
56 13 1 55 9 deg1lt0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑃 ) ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 ↔ 𝑎 = ( 0g ‘ 𝑃 ) ) )
57 54 12 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 ↔ 𝑎 = ( 0g ‘ 𝑃 ) ) )
58 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
59 4 58 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
60 2 55 lidl0cl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑃 ) ∈ 𝐼 )
61 59 5 60 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐼 )
62 eleq1a ⊢ ( ( 0g ‘ 𝑃 ) ∈ 𝐼 → ( 𝑎 = ( 0g ‘ 𝑃 ) → 𝑎 ∈ 𝐼 ) )
63 61 62 syl ⊢ ( 𝜑 → ( 𝑎 = ( 0g ‘ 𝑃 ) → 𝑎 ∈ 𝐼 ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( 𝑎 = ( 0g ‘ 𝑃 ) → 𝑎 ∈ 𝐼 ) )
65 57 64 sylbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 → 𝑎 ∈ 𝐼 ) )
66 65 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 0 → 𝑎 ∈ 𝐼 ) )
67 11 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → 𝐽 ⊆ ( Base ‘ 𝑃 ) )
68 67 sselda ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → 𝑑 ∈ ( Base ‘ 𝑃 ) )
69 13 1 9 deg1cl ⊢ ( 𝑑 ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( ℕ0 ∪ { -∞ } ) )
70 68 69 syl ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( ℕ0 ∪ { -∞ } ) )
71 simpl1 ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → 𝑏 ∈ ℕ0 )
72 71 nn0zd ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → 𝑏 ∈ ℤ )
73 degltp1le ⊢ ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑏 ∈ ℤ ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) )
74 70 72 73 syl2anc ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) )
75 fveq2 ⊢ ( 𝑥 = 𝑏 → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) )
76 fveq2 ⊢ ( 𝑥 = 𝑏 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) )
77 75 76 sseq12d ⊢ ( 𝑥 = 𝑏 → ( ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑥 ) ↔ ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) ) )
78 77 rspcva ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑥 ) ) → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) )
79 8 78 sylan2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) )
80 4 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → 𝑅 ∈ Ring )
81 6 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → 𝐽 ∈ 𝑈 )
82 simpl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → 𝑏 ∈ ℕ0 )
83 1 2 3 13 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ 𝑈 ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) = { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
84 80 81 82 83 syl3anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → ( ( 𝑆 ‘ 𝐽 ) ‘ 𝑏 ) = { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
85 5 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → 𝐼 ∈ 𝑈 )
86 1 2 3 13 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) = { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
87 80 85 82 86 syl3anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑏 ) = { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
88 79 84 87 3sstr3d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ) → { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } ⊆ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
89 88 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } ⊆ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
90 89 adantr ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } ⊆ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
91 simpl ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) → 𝑑 ∈ 𝐽 )
92 simpr ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 )
93 eqidd ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) → ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) )
94 fveq2 ⊢ ( 𝑒 = 𝑑 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) )
95 94 breq1d ⊢ ( 𝑒 = 𝑑 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) )
96 fveq2 ⊢ ( 𝑒 = 𝑑 → ( coe1 ‘ 𝑒 ) = ( coe1 ‘ 𝑑 ) )
97 96 fveq1d ⊢ ( 𝑒 = 𝑑 → ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) )
98 97 eqeq2d ⊢ ( 𝑒 = 𝑑 → ( ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ↔ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ) )
99 95 98 anbi12d ⊢ ( 𝑒 = 𝑑 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ) ) )
100 99 rspcev ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ) ) → ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) )
101 91 92 93 100 syl12anc ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) → ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) )
102 fvex ⊢ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ V
103 eqeq1 ⊢ ( 𝑐 = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) → ( 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ↔ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) )
104 103 anbi2d ⊢ ( 𝑐 = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) )
105 104 rexbidv ⊢ ( 𝑐 = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) → ( ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ↔ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) )
106 102 105 elab ⊢ ( ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } ↔ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) )
107 101 106 sylibr ⊢ ( ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) → ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
108 107 adantl ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
109 90 108 sseldd ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } )
110 104 rexbidv ⊢ ( 𝑐 = ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) → ( ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ↔ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) )
111 102 110 elab ⊢ ( ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } ↔ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) )
112 simpll2 ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝜑 )
113 112 59 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑃 ∈ Ring )
114 ringgrp ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
115 113 114 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑃 ∈ Grp )
116 112 11 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝐽 ⊆ ( Base ‘ 𝑃 ) )
117 simplrl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑑 ∈ 𝐽 )
118 116 117 sseldd ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑑 ∈ ( Base ‘ 𝑃 ) )
119 9 2 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
120 5 119 syl ⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
121 112 120 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
122 simprl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑒 ∈ 𝐼 )
123 121 122 sseldd ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑒 ∈ ( Base ‘ 𝑃 ) )
124 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
125 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
126 9 124 125 grpnpcan ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑑 ∈ ( Base ‘ 𝑃 ) ∧ 𝑒 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ( +g ‘ 𝑃 ) 𝑒 ) = 𝑑 )
127 115 118 123 126 syl3anc ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ( +g ‘ 𝑃 ) 𝑒 ) = 𝑑 )
128 5 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → 𝐼 ∈ 𝑈 )
129 128 ad2antrr ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝐼 ∈ 𝑈 )
130 simpll1 ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑏 ∈ ℕ0 )
131 112 4 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑅 ∈ Ring )
132 simplrr ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 )
133 simprrl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 )
134 eqid ⊢ ( coe1 ‘ 𝑑 ) = ( coe1 ‘ 𝑑 )
135 eqid ⊢ ( coe1 ‘ 𝑒 ) = ( coe1 ‘ 𝑒 )
136 simprrr ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) )
137 13 1 9 125 130 131 118 132 123 133 134 135 136 deg1sublt ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) < 𝑏 )
138 112 6 syl ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝐽 ∈ 𝑈 )
139 7 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → 𝐼 ⊆ 𝐽 )
140 139 ad2antrr ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝐼 ⊆ 𝐽 )
141 140 122 sseldd ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑒 ∈ 𝐽 )
142 2 125 lidlsubcl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐽 ∈ 𝑈 ) ∧ ( 𝑑 ∈ 𝐽 ∧ 𝑒 ∈ 𝐽 ) ) → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐽 )
143 113 138 117 141 142 syl22anc ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐽 )
144 simpll3 ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) )
145 fveq2 ⊢ ( 𝑎 = ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) )
146 145 breq1d ⊢ ( 𝑎 = ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) < 𝑏 ) )
147 eleq1 ⊢ ( 𝑎 = ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) → ( 𝑎 ∈ 𝐼 ↔ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 ) )
148 146 147 imbi12d ⊢ ( 𝑎 = ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) < 𝑏 → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 ) ) )
149 148 rspcva ⊢ ( ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐽 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) < 𝑏 → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 ) )
150 143 144 149 syl2anc ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ) < 𝑏 → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 ) )
151 137 150 mpd ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 )
152 2 124 lidlacl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 ∧ 𝑒 ∈ 𝐼 ) ) → ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ( +g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 )
153 113 129 151 122 152 syl22anc ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → ( ( 𝑑 ( -g ‘ 𝑃 ) 𝑒 ) ( +g ‘ 𝑃 ) 𝑒 ) ∈ 𝐼 )
154 127 153 eqeltrrd ⊢ ( ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) ) ) → 𝑑 ∈ 𝐼 )
155 154 rexlimdvaa ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → ( ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) → 𝑑 ∈ 𝐼 ) )
156 111 155 biimtrid ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → ( ( ( coe1 ‘ 𝑑 ) ‘ 𝑏 ) ∈ { 𝑐 ∣ ∃ 𝑒 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑒 ) ≤ 𝑏 ∧ 𝑐 = ( ( coe1 ‘ 𝑒 ) ‘ 𝑏 ) ) } → 𝑑 ∈ 𝐼 ) )
157 109 156 mpd ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ ( 𝑑 ∈ 𝐽 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 ) ) → 𝑑 ∈ 𝐼 )
158 157 expr ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) ≤ 𝑏 → 𝑑 ∈ 𝐼 ) )
159 74 158 sylbid ⊢ ( ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ∧ 𝑑 ∈ 𝐽 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) )
160 159 ralrimiva ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝜑 ∧ ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) )
161 160 3exp ⊢ ( 𝑏 ∈ ℕ0 → ( 𝜑 → ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) → ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) ) ) )
162 161 a2d ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) → ( 𝜑 → ∀ 𝑑 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑑 ) < ( 𝑏 + 1 ) → 𝑑 ∈ 𝐼 ) ) ) )
163 39 43 53 43 66 162 nn0ind ⊢ ( 𝑏 ∈ ℕ0 → ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) )
164 rsp ⊢ ( ∀ 𝑎 ∈ 𝐽 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) → ( 𝑎 ∈ 𝐽 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) )
165 163 164 syl6com ⊢ ( 𝜑 → ( 𝑏 ∈ ℕ0 → ( 𝑎 ∈ 𝐽 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ) )
166 165 com23 ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐽 → ( 𝑏 ∈ ℕ0 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) ) )
167 166 imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( 𝑏 ∈ ℕ0 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) ) )
168 167 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → ( ∃ 𝑏 ∈ ℕ0 ( ( deg1 ‘ 𝑅 ) ‘ 𝑎 ) < 𝑏 → 𝑎 ∈ 𝐼 ) )
169 35 168 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐽 ) → 𝑎 ∈ 𝐼 )
170 7 169 eqelssd ⊢ ( 𝜑 → 𝐼 = 𝐽 )