| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mpteq1 5234 | . . . . . 6
⊢ (𝑎 = ∅ → (𝑥 ∈ 𝑎 ↦ 𝐶) = (𝑥 ∈ ∅ ↦ 𝐶)) | 
| 2 | 1 | oveq2d 7448 | . . . . 5
⊢ (𝑎 = ∅ →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) | 
| 3 | 2 | fveq2d 6909 | . . . 4
⊢ (𝑎 = ∅ →
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)))) | 
| 4 |  | sumeq1 15726 | . . . 4
⊢ (𝑎 = ∅ → Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = Σ𝑛 ∈ ∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 5 | 3, 4 | eqeq12d 2752 | . . 3
⊢ (𝑎 = ∅ →
(((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ↔ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = Σ𝑛 ∈ ∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)))) | 
| 6 | 3 | breq2d 5154 | . . 3
⊢ (𝑎 = ∅ → (0 ≤
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) ↔ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))))) | 
| 7 | 5, 6 | anbi12d 632 | . 2
⊢ (𝑎 = ∅ →
((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)))) ↔ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = Σ𝑛 ∈ ∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)))))) | 
| 8 |  | mpteq1 5234 | . . . . . 6
⊢ (𝑎 = 𝑏 → (𝑥 ∈ 𝑎 ↦ 𝐶) = (𝑥 ∈ 𝑏 ↦ 𝐶)) | 
| 9 | 8 | oveq2d 7448 | . . . . 5
⊢ (𝑎 = 𝑏 →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) | 
| 10 | 9 | fveq2d 6909 | . . . 4
⊢ (𝑎 = 𝑏 → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶)))) | 
| 11 |  | sumeq1 15726 | . . . 4
⊢ (𝑎 = 𝑏 → Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 12 | 10, 11 | eqeq12d 2752 | . . 3
⊢ (𝑎 = 𝑏 → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ↔ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)))) | 
| 13 | 10 | breq2d 5154 | . . 3
⊢ (𝑎 = 𝑏 → (0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) ↔ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) | 
| 14 | 12, 13 | anbi12d 632 | . 2
⊢ (𝑎 = 𝑏 → ((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)))) ↔ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶)))))) | 
| 15 |  | mpteq1 5234 | . . . . . 6
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (𝑥 ∈ 𝑎 ↦ 𝐶) = (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) | 
| 16 | 15 | oveq2d 7448 | . . . . 5
⊢ (𝑎 = (𝑏 ∪ {𝑐}) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) | 
| 17 | 16 | fveq2d 6909 | . . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)))) | 
| 18 |  | sumeq1 15726 | . . . 4
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 19 | 17, 18 | eqeq12d 2752 | . . 3
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ↔ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)))) | 
| 20 | 17 | breq2d 5154 | . . 3
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → (0 ≤
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) ↔ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))))) | 
| 21 | 19, 20 | anbi12d 632 | . 2
⊢ (𝑎 = (𝑏 ∪ {𝑐}) → ((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)))) ↔ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)))))) | 
| 22 |  | mpteq1 5234 | . . . . . 6
⊢ (𝑎 = 𝑁 → (𝑥 ∈ 𝑎 ↦ 𝐶) = (𝑥 ∈ 𝑁 ↦ 𝐶)) | 
| 23 | 22 | oveq2d 7448 | . . . . 5
⊢ (𝑎 = 𝑁 →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))) | 
| 24 | 23 | fveq2d 6909 | . . . 4
⊢ (𝑎 = 𝑁 → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶)))) | 
| 25 |  | sumeq1 15726 | . . . 4
⊢ (𝑎 = 𝑁 → Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = Σ𝑛 ∈ 𝑁 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 26 | 24, 25 | eqeq12d 2752 | . . 3
⊢ (𝑎 = 𝑁 → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ↔ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))) = Σ𝑛 ∈ 𝑁 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)))) | 
| 27 | 24 | breq2d 5154 | . . 3
⊢ (𝑎 = 𝑁 → (0 ≤
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) ↔ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))))) | 
| 28 | 26, 27 | anbi12d 632 | . 2
⊢ (𝑎 = 𝑁 → ((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶))) = Σ𝑛 ∈ 𝑎 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑎 ↦ 𝐶)))) ↔ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))) = Σ𝑛 ∈ 𝑁 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶)))))) | 
| 29 |  | mpt0 6709 | . . . . . . . . 9
⊢ (𝑥 ∈ ∅ ↦ 𝐶) = ∅ | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ∅ ↦ 𝐶) = ∅) | 
| 31 | 30 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg
∅)) | 
| 32 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘(mulGrp‘(Poly1‘𝑅))) =
(0g‘(mulGrp‘(Poly1‘𝑅))) | 
| 33 | 32 | gsum0 18698 | . . . . . . . 8
⊢
((mulGrp‘(Poly1‘𝑅)) Σg ∅) =
(0g‘(mulGrp‘(Poly1‘𝑅))) | 
| 34 | 33 | a1i 11 | . . . . . . 7
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝑅)) Σg ∅) =
(0g‘(mulGrp‘(Poly1‘𝑅)))) | 
| 35 | 31, 34 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)) =
(0g‘(mulGrp‘(Poly1‘𝑅)))) | 
| 36 | 35 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = ((deg1‘𝑅)‘(0g‘(mulGrp‘(Poly1‘𝑅))))) | 
| 37 |  | deg1gprod.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 38 | 37 | idomringd 20729 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 39 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) | 
| 40 |  | eqid 2736 | . . . . . . . . . 10
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) | 
| 41 |  | eqid 2736 | . . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 42 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(mulGrp‘(Poly1‘𝑅)) =
(mulGrp‘(Poly1‘𝑅)) | 
| 43 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(1r‘(Poly1‘𝑅)) =
(1r‘(Poly1‘𝑅)) | 
| 44 | 42, 43 | ringidval 20181 | . . . . . . . . . . 11
⊢
(1r‘(Poly1‘𝑅)) =
(0g‘(mulGrp‘(Poly1‘𝑅))) | 
| 45 | 44 | eqcomi 2745 | . . . . . . . . . 10
⊢
(0g‘(mulGrp‘(Poly1‘𝑅))) =
(1r‘(Poly1‘𝑅)) | 
| 46 | 39, 40, 41, 45 | ply1scl1 22297 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring →
((algSc‘(Poly1‘𝑅))‘(1r‘𝑅)) =
(0g‘(mulGrp‘(Poly1‘𝑅)))) | 
| 47 | 38, 46 | syl 17 | . . . . . . . 8
⊢ (𝜑 →
((algSc‘(Poly1‘𝑅))‘(1r‘𝑅)) =
(0g‘(mulGrp‘(Poly1‘𝑅)))) | 
| 48 | 47 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 →
(0g‘(mulGrp‘(Poly1‘𝑅))) =
((algSc‘(Poly1‘𝑅))‘(1r‘𝑅))) | 
| 49 | 48 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
((deg1‘𝑅)‘(0g‘(mulGrp‘(Poly1‘𝑅)))) = ((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘(1r‘𝑅)))) | 
| 50 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 51 | 50, 41 | ringidcl 20263 | . . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 52 | 38, 51 | syl 17 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 53 | 37 | idomdomd 20727 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Domn) | 
| 54 |  | domnnzr 20707 | . . . . . . . . 9
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) | 
| 55 | 53, 54 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ NzRing) | 
| 56 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 57 | 41, 56 | nzrnz 20516 | . . . . . . . 8
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ (0g‘𝑅)) | 
| 58 | 55, 57 | syl 17 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) | 
| 59 |  | eqid 2736 | . . . . . . . 8
⊢
(deg1‘𝑅) = (deg1‘𝑅) | 
| 60 | 59, 39, 50, 40, 56 | deg1scl 26153 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ (Base‘𝑅) ∧
(1r‘𝑅)
≠ (0g‘𝑅)) → ((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘(1r‘𝑅))) = 0) | 
| 61 | 38, 52, 58, 60 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 →
((deg1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘(1r‘𝑅))) = 0) | 
| 62 | 49, 61 | eqtrd 2776 | . . . . 5
⊢ (𝜑 →
((deg1‘𝑅)‘(0g‘(mulGrp‘(Poly1‘𝑅)))) = 0) | 
| 63 | 36, 62 | eqtrd 2776 | . . . 4
⊢ (𝜑 →
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = 0) | 
| 64 |  | sum0 15758 | . . . . . 6
⊢
Σ𝑛 ∈
∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = 0 | 
| 65 | 64 | eqcomi 2745 | . . . . 5
⊢ 0 =
Σ𝑛 ∈ ∅
((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) | 
| 66 | 65 | a1i 11 | . . . 4
⊢ (𝜑 → 0 = Σ𝑛 ∈ ∅
((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 67 | 63, 66 | eqtrd 2776 | . . 3
⊢ (𝜑 →
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = Σ𝑛 ∈ ∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 68 |  | 0red 11265 | . . . . 5
⊢ (𝜑 → 0 ∈
ℝ) | 
| 69 | 68 | leidd 11830 | . . . 4
⊢ (𝜑 → 0 ≤ 0) | 
| 70 | 63 | eqcomd 2742 | . . . 4
⊢ (𝜑 → 0 =
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)))) | 
| 71 | 69, 70 | breqtrd 5168 | . . 3
⊢ (𝜑 → 0 ≤
((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶)))) | 
| 72 | 67, 71 | jca 511 | . 2
⊢ (𝜑 →
(((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))) = Σ𝑛 ∈ ∅ ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ ∅ ↦ 𝐶))))) | 
| 73 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑦𝐶 | 
| 74 |  | nfcsb1v 3922 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 | 
| 75 |  | csbeq1a 3912 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) | 
| 76 | 73, 74, 75 | cbvmpt 5252 | . . . . . . . 8
⊢ (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶) = (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶) | 
| 77 | 76 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶) = (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶)) | 
| 78 | 77 | oveq2d 7448 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) = ((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶))) | 
| 79 | 78 | fveq2d 6909 | . . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶)))) | 
| 80 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(mulGrp‘(Poly1‘𝑅))) =
(Base‘(mulGrp‘(Poly1‘𝑅))) | 
| 81 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘(mulGrp‘(Poly1‘𝑅))) =
(+g‘(mulGrp‘(Poly1‘𝑅))) | 
| 82 |  | isidom 20726 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | 
| 83 | 37, 82 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | 
| 84 | 83 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 85 | 39 | ply1crng 22201 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(Poly1‘𝑅)
∈ CRing) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(Poly1‘𝑅)
∈ CRing) | 
| 87 | 42 | crngmgp 20239 | . . . . . . . . . . 11
⊢
((Poly1‘𝑅) ∈ CRing →
(mulGrp‘(Poly1‘𝑅)) ∈ CMnd) | 
| 88 | 86, 87 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 →
(mulGrp‘(Poly1‘𝑅)) ∈ CMnd) | 
| 89 | 88 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) →
(mulGrp‘(Poly1‘𝑅)) ∈ CMnd) | 
| 90 | 89 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
(mulGrp‘(Poly1‘𝑅)) ∈ CMnd) | 
| 91 |  | deg1gprod.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ Fin) | 
| 92 | 91 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑁 ∈ Fin) | 
| 93 |  | simplrl 776 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑏 ⊆ 𝑁) | 
| 94 | 92, 93 | ssfid 9302 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑏 ∈ Fin) | 
| 95 | 93 | sselda 3982 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → 𝑦 ∈ 𝑁) | 
| 96 |  | deg1gprod.3 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ 𝐶 ≠
(0g‘(Poly1‘𝑅)))) | 
| 97 |  | r19.26 3110 | . . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑁 (𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ 𝐶 ≠
(0g‘(Poly1‘𝑅))) ↔ (∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅)))) | 
| 98 | 97 | biimpi 216 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑁 (𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ 𝐶 ≠
(0g‘(Poly1‘𝑅))) → (∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅)))) | 
| 99 | 96, 98 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅)))) | 
| 100 | 99 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 101 | 100 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → ∀𝑥 ∈ 𝑁 𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 102 |  | rspcsbela 4437 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) → ⦋𝑦 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 103 | 95, 101, 102 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → ⦋𝑦 / 𝑥⦌𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 104 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) | 
| 105 | 42, 104 | mgpbas 20143 | . . . . . . . . 9
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(mulGrp‘(Poly1‘𝑅))) | 
| 106 | 103, 105 | eleqtrdi 2850 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → ⦋𝑦 / 𝑥⦌𝐶 ∈
(Base‘(mulGrp‘(Poly1‘𝑅)))) | 
| 107 |  | eldifi 4130 | . . . . . . . . . . 11
⊢ (𝑐 ∈ (𝑁 ∖ 𝑏) → 𝑐 ∈ 𝑁) | 
| 108 | 107 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏)) → 𝑐 ∈ 𝑁) | 
| 109 | 108 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑐 ∈ 𝑁) | 
| 110 | 109 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑐 ∈ 𝑁) | 
| 111 |  | eldifn 4131 | . . . . . . . . . . 11
⊢ (𝑐 ∈ (𝑁 ∖ 𝑏) → ¬ 𝑐 ∈ 𝑏) | 
| 112 | 111 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏)) → ¬ 𝑐 ∈ 𝑏) | 
| 113 | 112 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ¬ 𝑐 ∈ 𝑏) | 
| 114 | 113 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ¬ 𝑐 ∈ 𝑏) | 
| 115 | 100 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ∀𝑥 ∈ 𝑁 𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 116 |  | rspcsbela 4437 | . . . . . . . . . 10
⊢ ((𝑐 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) → ⦋𝑐 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 117 | 110, 115,
116 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ⦋𝑐 / 𝑥⦌𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 118 | 117, 105 | eleqtrdi 2850 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ⦋𝑐 / 𝑥⦌𝐶 ∈
(Base‘(mulGrp‘(Poly1‘𝑅)))) | 
| 119 |  | csbeq1 3901 | . . . . . . . 8
⊢ (𝑦 = 𝑐 → ⦋𝑦 / 𝑥⦌𝐶 = ⦋𝑐 / 𝑥⦌𝐶) | 
| 120 | 80, 81, 90, 94, 106, 110, 114, 118, 119 | gsumunsn 19979 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶)) = (((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))(+g‘(mulGrp‘(Poly1‘𝑅)))⦋𝑐 / 𝑥⦌𝐶)) | 
| 121 | 120 | fveq2d 6909 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶))) = ((deg1‘𝑅)‘(((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))(+g‘(mulGrp‘(Poly1‘𝑅)))⦋𝑐 / 𝑥⦌𝐶))) | 
| 122 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘(Poly1‘𝑅)) =
(.r‘(Poly1‘𝑅)) | 
| 123 | 42, 122 | mgpplusg 20142 | . . . . . . . . 9
⊢
(.r‘(Poly1‘𝑅)) =
(+g‘(mulGrp‘(Poly1‘𝑅))) | 
| 124 | 123 | eqcomi 2745 | . . . . . . . 8
⊢
(+g‘(mulGrp‘(Poly1‘𝑅))) =
(.r‘(Poly1‘𝑅)) | 
| 125 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘(Poly1‘𝑅)) =
(0g‘(Poly1‘𝑅)) | 
| 126 | 53 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑅 ∈ Domn) | 
| 127 | 126 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑅 ∈ Domn) | 
| 128 | 103 | ralrimiva 3145 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ∀𝑦 ∈ 𝑏 ⦋𝑦 / 𝑥⦌𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 129 | 105, 90, 94, 128 | gsummptcl 19986 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶)) ∈ (Base‘(Poly1‘𝑅))) | 
| 130 | 39 | ply1idom 26165 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ IDomn →
(Poly1‘𝑅)
∈ IDomn) | 
| 131 | 37, 130 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(Poly1‘𝑅)
∈ IDomn) | 
| 132 | 131 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → (Poly1‘𝑅) ∈ IDomn) | 
| 133 | 132 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (Poly1‘𝑅) ∈ IDomn) | 
| 134 | 99 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 135 | 134 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 136 |  | rspcsbnea 42133 | . . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) → ⦋𝑦 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 137 | 95, 135, 136 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) ∧ 𝑦 ∈ 𝑏) → ⦋𝑦 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 138 | 42, 133, 94, 103, 137 | idomnnzgmulnz 42135 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶)) ≠
(0g‘(Poly1‘𝑅))) | 
| 139 | 134 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 140 |  | rspcsbnea 42133 | . . . . . . . . 9
⊢ ((𝑐 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) → ⦋𝑐 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 141 | 110, 139,
140 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ⦋𝑐 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 142 | 59, 39, 104, 124, 125, 127, 129, 138, 117, 141 | deg1mul 26155 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘(((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))(+g‘(mulGrp‘(Poly1‘𝑅)))⦋𝑐 / 𝑥⦌𝐶)) = (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏
↦ ⦋𝑦 / 𝑥⦌𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶))) | 
| 143 | 73, 74, 75 | cbvmpt 5252 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑏 ↦ 𝐶) = (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶) | 
| 144 | 143 | eqcomi 2745 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶) = (𝑥 ∈ 𝑏 ↦ 𝐶) | 
| 145 | 144 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶) = (𝑥 ∈ 𝑏 ↦ 𝐶)) | 
| 146 | 145 | oveq2d 7448 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶)) = ((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) | 
| 147 | 146 | fveq2d 6909 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))) = ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶)))) | 
| 148 | 147 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) = (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶))) | 
| 149 |  | simpl 482 | . . . . . . . . . . 11
⊢
((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶)))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 150 | 149 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 151 | 150 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) = (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶))) | 
| 152 |  | nfv 1913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) | 
| 153 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)) | 
| 154 | 91 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑁 ∈ Fin) | 
| 155 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑏 ⊆ 𝑁) | 
| 156 | 154, 155 | ssfid 9302 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑏 ∈ Fin) | 
| 157 | 73, 74, 75 | cbvmpt 5252 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑁 ↦ 𝐶) = (𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶) | 
| 158 | 157 | fveq1i 6906 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛) = ((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛) | 
| 159 | 158 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛) = ((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛)) | 
| 160 | 159 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = ((deg1‘𝑅)‘((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛))) | 
| 161 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → (𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶) = (𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)) | 
| 162 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) ∧ 𝑦 = 𝑛) → 𝑦 = 𝑛) | 
| 163 | 162 | csbeq1d 3902 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) ∧ 𝑦 = 𝑛) → ⦋𝑦 / 𝑥⦌𝐶 = ⦋𝑛 / 𝑥⦌𝐶) | 
| 164 | 155 | sselda 3982 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → 𝑛 ∈ 𝑁) | 
| 165 | 100 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 166 | 165 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 167 |  | rspcsbela 4437 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) → ⦋𝑛 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 168 | 164, 166,
167 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ⦋𝑛 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 169 | 161, 163,
164, 168 | fvmptd 7022 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛) = ⦋𝑛 / 𝑥⦌𝐶) | 
| 170 | 169 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛)) = ((deg1‘𝑅)‘⦋𝑛 / 𝑥⦌𝐶)) | 
| 171 | 38 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → 𝑅 ∈ Ring) | 
| 172 | 171 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → 𝑅 ∈ Ring) | 
| 173 | 134 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 174 |  | rspcsbnea 42133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) → ⦋𝑛 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 175 | 164, 173,
174 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ⦋𝑛 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 176 | 59, 39, 125, 104 | deg1nn0cl 26128 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧
⦋𝑛 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ ⦋𝑛 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) → ((deg1‘𝑅)‘⦋𝑛 / 𝑥⦌𝐶) ∈
ℕ0) | 
| 177 | 172, 168,
175, 176 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘⦋𝑛 / 𝑥⦌𝐶) ∈
ℕ0) | 
| 178 | 170, 177 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘((𝑦 ∈ 𝑁 ↦ ⦋𝑦 / 𝑥⦌𝐶)‘𝑛)) ∈
ℕ0) | 
| 179 | 160, 178 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∈
ℕ0) | 
| 180 | 179 | nn0cnd 12591 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑛 ∈ 𝑏) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∈ ℂ) | 
| 181 |  | 2fveq3 6910 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑐 → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐))) | 
| 182 | 109, 165,
116 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ⦋𝑐 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 183 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑁 ↦ 𝐶) = (𝑥 ∈ 𝑁 ↦ 𝐶) | 
| 184 | 183 | fvmpts 7018 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ 𝑁 ∧ ⦋𝑐 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) → ((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐) = ⦋𝑐 / 𝑥⦌𝐶) | 
| 185 | 109, 182,
184 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐) = ⦋𝑐 / 𝑥⦌𝐶) | 
| 186 | 185 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)) = ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) | 
| 187 | 108, 134,
140 | syl2anr 597 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ⦋𝑐 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 188 | 59, 39, 125, 104 | deg1nn0cl 26128 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧
⦋𝑐 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅)) ∧ ⦋𝑐 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) → ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶) ∈
ℕ0) | 
| 189 | 171, 182,
187, 188 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶) ∈
ℕ0) | 
| 190 | 186, 189 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)) ∈
ℕ0) | 
| 191 | 190 | nn0cnd 12591 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)) ∈ ℂ) | 
| 192 | 152, 153,
156, 109, 113, 180, 181, 191 | fsumsplitsn 15781 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)))) | 
| 193 | 192 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)))) | 
| 194 | 185 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐) = ⦋𝑐 / 𝑥⦌𝐶) | 
| 195 | 194 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐)) = ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) | 
| 196 | 195 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑐))) = (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶))) | 
| 197 | 193, 196 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) = (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶))) | 
| 198 | 197 | eqcomd 2742 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 199 | 151, 198 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 200 | 148, 199 | eqtrd 2776 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))) + ((deg1‘𝑅)‘⦋𝑐 / 𝑥⦌𝐶)) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 201 | 142, 200 | eqtrd 2776 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘(((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ 𝑏 ↦ ⦋𝑦 / 𝑥⦌𝐶))(+g‘(mulGrp‘(Poly1‘𝑅)))⦋𝑐 / 𝑥⦌𝐶)) = Σ𝑛
∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥
∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 202 | 121, 201 | eqtrd 2776 | . . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 203 | 79, 202 | eqtrd 2776 | . . . 4
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛))) | 
| 204 | 171 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 𝑅 ∈ Ring) | 
| 205 | 110 | snssd 4808 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → {𝑐} ⊆ 𝑁) | 
| 206 | 93, 205 | unssd 4191 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (𝑏 ∪ {𝑐}) ⊆ 𝑁) | 
| 207 | 92, 206 | ssfid 9302 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (𝑏 ∪ {𝑐}) ∈ Fin) | 
| 208 | 165 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ∀𝑥 ∈ 𝑁 𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 209 |  | ssralv 4051 | . . . . . . . . 9
⊢ ((𝑏 ∪ {𝑐}) ⊆ 𝑁 → (∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅)) → ∀𝑥 ∈ (𝑏 ∪ {𝑐})𝐶 ∈
(Base‘(Poly1‘𝑅)))) | 
| 210 | 206, 209 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (∀𝑥 ∈ 𝑁 𝐶 ∈ (Base‘(Poly1‘𝑅)) → ∀𝑥 ∈ (𝑏 ∪ {𝑐})𝐶 ∈ (Base‘(Poly1‘𝑅)))) | 
| 211 | 208, 210 | mpd 15 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ∀𝑥 ∈ (𝑏 ∪ {𝑐})𝐶 ∈ (Base‘(Poly1‘𝑅))) | 
| 212 | 105, 90, 207, 211 | gsummptcl 19986 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) ∈ (Base‘(Poly1‘𝑅))) | 
| 213 | 76 | oveq2i 7443 | . . . . . . . . 9
⊢
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶)) | 
| 214 | 213 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) =
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶))) | 
| 215 | 109 | snssd 4808 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → {𝑐} ⊆ 𝑁) | 
| 216 | 155, 215 | unssd 4191 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → (𝑏 ∪ {𝑐}) ⊆ 𝑁) | 
| 217 | 154, 216 | ssfid 9302 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → (𝑏 ∪ {𝑐}) ∈ Fin) | 
| 218 | 216 | sselda 3982 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑦 ∈ (𝑏 ∪ {𝑐})) → 𝑦 ∈ 𝑁) | 
| 219 | 165 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑦 ∈ (𝑏 ∪ {𝑐})) → ∀𝑥 ∈ 𝑁 𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 220 | 218, 219,
102 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑦 ∈ (𝑏 ∪ {𝑐})) → ⦋𝑦 / 𝑥⦌𝐶 ∈
(Base‘(Poly1‘𝑅))) | 
| 221 | 134 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑦 ∈ (𝑏 ∪ {𝑐})) → ∀𝑥 ∈ 𝑁 𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 222 | 218, 221,
136 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ 𝑦 ∈ (𝑏 ∪ {𝑐})) → ⦋𝑦 / 𝑥⦌𝐶 ≠
(0g‘(Poly1‘𝑅))) | 
| 223 | 42, 132, 217, 220, 222 | idomnnzgmulnz 42135 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑦 ∈ (𝑏 ∪ {𝑐}) ↦ ⦋𝑦 / 𝑥⦌𝐶)) ≠
(0g‘(Poly1‘𝑅))) | 
| 224 | 214, 223 | eqnetrd 3007 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) ≠
(0g‘(Poly1‘𝑅))) | 
| 225 | 224 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) →
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) ≠
(0g‘(Poly1‘𝑅))) | 
| 226 | 59, 39, 125, 104 | deg1nn0cl 26128 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) ∈
(Base‘(Poly1‘𝑅)) ∧
((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)) ≠
(0g‘(Poly1‘𝑅))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) ∈ ℕ0) | 
| 227 | 204, 212,
225, 226 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) ∈ ℕ0) | 
| 228 | 227 | nn0ge0d 12592 | . . . 4
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)))) | 
| 229 | 203, 228 | jca 511 | . . 3
⊢ (((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) ∧ (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))))) | 
| 230 | 229 | ex 412 | . 2
⊢ ((𝜑 ∧ (𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ (𝑁 ∖ 𝑏))) → ((((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶))) = Σ𝑛 ∈ 𝑏 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑏 ↦ 𝐶)))) → (((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶))) = Σ𝑛 ∈ (𝑏 ∪ {𝑐})((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ (𝑏 ∪ {𝑐}) ↦ 𝐶)))))) | 
| 231 | 7, 14, 21, 28, 72, 230, 91 | findcard2d 9207 | 1
⊢ (𝜑 →
(((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))) = Σ𝑛 ∈ 𝑁 ((deg1‘𝑅)‘((𝑥 ∈ 𝑁 ↦ 𝐶)‘𝑛)) ∧ 0 ≤ ((deg1‘𝑅)‘((mulGrp‘(Poly1‘𝑅)) Σg (𝑥 ∈ 𝑁 ↦ 𝐶))))) |