Metamath Proof Explorer

Theorem hbtlem2

Description: Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem2.t ⊢ 𝑇 = ( LIdeal ‘ 𝑅 )
Assertion hbtlem2 ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem2.t ⊢ 𝑇 = ( LIdeal ‘ 𝑅 )
5 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
6 1 2 3 5 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
7 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 7 2 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
9 8 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
10 9 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑃 ) )
11 eqid ⊢ ( coe1 ‘ 𝑏 ) = ( coe1 ‘ 𝑏 )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 11 7 1 12 coe1f ⊢ ( 𝑏 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑏 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
14 10 13 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → ( coe1 ‘ 𝑏 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
15 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → 𝑋 ∈ ℕ0 )
16 14 15 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
17 eleq1a ⊢ ( ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
18 16 17 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
19 18 adantld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑏 ∈ 𝐼 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
20 19 rexlimdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
21 20 abssdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ⊆ ( Base ‘ 𝑅 ) )
22 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
23 22 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → 𝑃 ∈ Ring )
24 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → 𝐼 ∈ 𝑈 )
25 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
26 2 25 lidl0cl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑃 ) ∈ 𝐼 )
27 23 24 26 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( 0g ‘ 𝑃 ) ∈ 𝐼 )
28 5 1 25 deg1z ⊢ ( 𝑅 ∈ Ring → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
29 28 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
30 nn0ssre ⊢ ℕ0 ⊆ ℝ
31 ressxr ⊢ ℝ ⊆ ℝ*
32 30 31 sstri ⊢ ℕ0 ⊆ ℝ*
33 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℕ0 )
34 32 33 sselid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℝ* )
35 mnfle ⊢ ( 𝑋 ∈ ℝ* → -∞ ≤ 𝑋 )
36 34 35 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → -∞ ≤ 𝑋 )
37 29 36 eqbrtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) ≤ 𝑋 )
38 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
39 1 25 38 coe1z ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ ( 0g ‘ 𝑃 ) ) = ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) )
40 39 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( coe1 ‘ ( 0g ‘ 𝑃 ) ) = ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) )
41 40 fveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) = ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑋 ) )
42 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
43 42 fvconst2 ⊢ ( 𝑋 ∈ ℕ0 → ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑋 ) = ( 0g ‘ 𝑅 ) )
44 43 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑋 ) = ( 0g ‘ 𝑅 ) )
45 41 44 eqtr2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) )
46 fveq2 ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) )
47 46 breq1d ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) ≤ 𝑋 ) )
48 fveq2 ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( coe1 ‘ 𝑏 ) = ( coe1 ‘ ( 0g ‘ 𝑃 ) ) )
49 48 fveq1d ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) )
50 49 eqeq2d ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) ) )
51 47 50 anbi12d ⊢ ( 𝑏 = ( 0g ‘ 𝑃 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) ) ) )
52 51 rspcev ⊢ ( ( ( 0g ‘ 𝑃 ) ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝑋 ) ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
53 27 37 45 52 syl12anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
54 eqeq1 ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
55 54 anbi2d ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
56 55 rexbidv ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
57 42 56 elab ⊢ ( ( 0g ‘ 𝑅 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( 0g ‘ 𝑅 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
58 53 57 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
59 58 ne0d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ≠ ∅ )
60 23 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑃 ∈ Ring )
61 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝐼 ∈ 𝑈 )
62 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
63 1 62 12 7 ply1sclf ⊢ ( 𝑅 ∈ Ring → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
64 63 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
65 64 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( algSc ‘ 𝑃 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
66 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
67 65 66 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ∈ ( Base ‘ 𝑃 ) )
68 simprll ⊢ ( ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) → 𝑓 ∈ 𝐼 )
69 68 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑓 ∈ 𝐼 )
70 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
71 2 7 70 lidlmcl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑓 ∈ 𝐼 ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ 𝐼 )
72 60 61 67 69 71 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ 𝐼 )
73 simprrl ⊢ ( ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) → 𝑔 ∈ 𝐼 )
74 73 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑔 ∈ 𝐼 )
75 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
76 2 75 lidlacl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ 𝐼 ∧ 𝑔 ∈ 𝐼 ) ) → ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ∈ 𝐼 )
77 60 61 72 74 76 syl22anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ∈ 𝐼 )
78 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑅 ∈ Ring )
79 9 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
80 79 69 sseldd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑓 ∈ ( Base ‘ 𝑃 ) )
81 7 70 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑓 ∈ ( Base ‘ 𝑃 ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ ( Base ‘ 𝑃 ) )
82 60 67 80 81 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ ( Base ‘ 𝑃 ) )
83 79 74 sseldd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑔 ∈ ( Base ‘ 𝑃 ) )
84 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑋 ∈ ℕ0 )
85 32 84 sselid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → 𝑋 ∈ ℝ* )
86 5 1 7 deg1xrcl ⊢ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ∈ ℝ* )
87 82 86 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ∈ ℝ* )
88 5 1 7 deg1xrcl ⊢ ( 𝑓 ∈ ( Base ‘ 𝑃 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ∈ ℝ* )
89 80 88 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ∈ ℝ* )
90 5 1 12 7 70 62 deg1mul3le ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ≤ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) )
91 78 66 80 90 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ≤ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) )
92 simprlr ⊢ ( ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 )
93 92 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 )
94 87 89 85 91 93 xrletrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ≤ 𝑋 )
95 simprrr ⊢ ( ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 )
96 95 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 )
97 1 5 78 7 75 82 83 85 94 96 deg1addle2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ≤ 𝑋 )
98 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
99 1 7 75 98 coe1addfv ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑔 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
100 78 82 83 84 99 syl31anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) = ( ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
101 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
102 1 7 12 62 70 101 coe1sclmulfv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑋 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ‘ 𝑋 ) = ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) )
103 78 66 80 84 102 syl121anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ‘ 𝑋 ) = ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) )
104 103 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
105 100 104 eqtr2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) )
106 fveq2 ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) = ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) )
107 106 breq1d ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ≤ 𝑋 ) )
108 fveq2 ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( coe1 ‘ 𝑏 ) = ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) )
109 108 fveq1d ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) )
110 109 eqeq2d ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) ) )
111 107 110 anbi12d ⊢ ( 𝑏 = ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) ) ) )
112 111 rspcev ⊢ ( ( ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ( .r ‘ 𝑃 ) 𝑓 ) ( +g ‘ 𝑃 ) 𝑔 ) ) ‘ 𝑋 ) ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
113 77 97 105 112 syl12anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
114 ovex ⊢ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ V
115 eqeq1 ⊢ ( 𝑎 = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
116 115 anbi2d ⊢ ( 𝑎 = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
117 116 rexbidv ⊢ ( 𝑎 = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
118 114 117 elab ⊢ ( ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
119 113 118 sylibr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) ) ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
120 119 exp45 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) → ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ( ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) ) ) )
121 120 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑓 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ( ( 𝑔 ∈ 𝐼 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) ) )
122 121 exp5c ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑓 ∈ 𝐼 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 → ( 𝑔 ∈ 𝐼 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) ) ) ) )
123 122 imp ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 → ( 𝑔 ∈ 𝐼 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) ) ) )
124 123 imp41 ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑔 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
125 oveq2 ⊢ ( 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
126 125 eleq1d ⊢ ( 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
127 124 126 syl5ibrcom ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑔 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) → ( 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
128 127 expimpd ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) ∧ 𝑔 ∈ 𝐼 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
129 128 rexlimdva ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ( ∃ 𝑔 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
130 129 alrimiv ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ∀ 𝑒 ( ∃ 𝑔 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
131 eqeq1 ⊢ ( 𝑎 = 𝑒 → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
132 131 anbi2d ⊢ ( 𝑎 = 𝑒 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
133 132 rexbidv ⊢ ( 𝑎 = 𝑒 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
134 fveq2 ⊢ ( 𝑏 = 𝑔 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) )
135 134 breq1d ⊢ ( 𝑏 = 𝑔 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ) )
136 fveq2 ⊢ ( 𝑏 = 𝑔 → ( coe1 ‘ 𝑏 ) = ( coe1 ‘ 𝑔 ) )
137 136 fveq1d ⊢ ( 𝑏 = 𝑔 → ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) )
138 137 eqeq2d ⊢ ( 𝑏 = 𝑔 → ( 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
139 135 138 anbi12d ⊢ ( 𝑏 = 𝑔 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ) )
140 139 cbvrexvw ⊢ ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑔 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) )
141 133 140 bitrdi ⊢ ( 𝑎 = 𝑒 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑔 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) ) )
142 141 ralab ⊢ ( ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ∀ 𝑒 ( ∃ 𝑔 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑔 ) ‘ 𝑋 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
143 130 142 sylibr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
144 oveq2 ⊢ ( 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) = ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) )
145 144 oveq1d ⊢ ( 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) = ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) )
146 145 eleq1d ⊢ ( 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
147 146 ralbidv ⊢ ( 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) → ( ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
148 143 147 syl5ibrcom ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) → ( 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
149 148 expimpd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑓 ∈ 𝐼 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
150 149 rexlimdva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ∃ 𝑓 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
151 150 alrimiv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑑 ( ∃ 𝑓 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
152 eqeq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
153 152 anbi2d ⊢ ( 𝑎 = 𝑑 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
154 153 rexbidv ⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ) )
155 fveq2 ⊢ ( 𝑏 = 𝑓 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) )
156 155 breq1d ⊢ ( 𝑏 = 𝑓 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ) )
157 fveq2 ⊢ ( 𝑏 = 𝑓 → ( coe1 ‘ 𝑏 ) = ( coe1 ‘ 𝑓 ) )
158 157 fveq1d ⊢ ( 𝑏 = 𝑓 → ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) )
159 158 eqeq2d ⊢ ( 𝑏 = 𝑓 → ( 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) )
160 156 159 anbi12d ⊢ ( 𝑏 = 𝑓 → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ) )
161 160 cbvrexvw ⊢ ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑓 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) )
162 154 161 bitrdi ⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↔ ∃ 𝑓 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) ) )
163 162 ralab ⊢ ( ∀ 𝑑 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ↔ ∀ 𝑑 ( ∃ 𝑓 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑓 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑓 ) ‘ 𝑋 ) ) → ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
164 151 163 sylibr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑑 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
165 164 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ∀ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑑 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
166 4 12 98 101 islidl ⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∈ 𝑇 ↔ ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ⊆ ( Base ‘ 𝑅 ) ∧ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ≠ ∅ ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑑 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∀ 𝑒 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( +g ‘ 𝑅 ) 𝑒 ) ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ) )
167 21 59 165 166 syl3anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } ∈ 𝑇 )
168 6 167 eqeltrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ 𝑇 )