deg1gprod

Description: Degree multiplication is a homomorphism. (Contributed by metakunt, 6-May-2025)

	Ref	Expression
Hypotheses	deg1gprod.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	deg1gprod.2	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	deg1gprod.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 ( 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
Assertion	deg1gprod	⊢ ( 𝜑 → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑁 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		deg1gprod.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2		deg1gprod.2	⊢ ( 𝜑 → 𝑁 ∈ Fin )
3		deg1gprod.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 ( 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
4		mpteq1	⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) = ( 𝑥 ∈ ∅ ↦ 𝐶 ) )
5	4	oveq2d	⊢ ( 𝑎 = ∅ → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) )
6	5	fveq2d	⊢ ( 𝑎 = ∅ → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) )
7		sumeq1	⊢ ( 𝑎 = ∅ → Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
8	6 7	eqeq12d	⊢ ( 𝑎 = ∅ → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ↔ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ) )
9	6	breq2d	⊢ ( 𝑎 = ∅ → ( 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ↔ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) ) )
10	8 9	anbi12d	⊢ ( 𝑎 = ∅ → ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ) ↔ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) ) ) )
11		mpteq1	⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) )
12	11	oveq2d	⊢ ( 𝑎 = 𝑏 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) )
13	12	fveq2d	⊢ ( 𝑎 = 𝑏 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) )
14		sumeq1	⊢ ( 𝑎 = 𝑏 → Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
15	13 14	eqeq12d	⊢ ( 𝑎 = 𝑏 → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ↔ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ) )
16	13	breq2d	⊢ ( 𝑎 = 𝑏 → ( 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ↔ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) )
17	15 16	anbi12d	⊢ ( 𝑎 = 𝑏 → ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ) ↔ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) )
18		mpteq1	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) )
19	18	oveq2d	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) )
20	19	fveq2d	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) )
21		sumeq1	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
22	20 21	eqeq12d	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ↔ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ) )
23	20	breq2d	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ↔ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ) )
24	22 23	anbi12d	⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ) ↔ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ) ) )
25		mpteq1	⊢ ( 𝑎 = 𝑁 → ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) )
26	25	oveq2d	⊢ ( 𝑎 = 𝑁 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) )
27	26	fveq2d	⊢ ( 𝑎 = 𝑁 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) )
28		sumeq1	⊢ ( 𝑎 = 𝑁 → Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = Σ 𝑛 ∈ 𝑁 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
29	27 28	eqeq12d	⊢ ( 𝑎 = 𝑁 → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ↔ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑁 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ) )
30	27	breq2d	⊢ ( 𝑎 = 𝑁 → ( 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ↔ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) ) )
31	29 30	anbi12d	⊢ ( 𝑎 = 𝑁 → ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑎 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑎 ↦ 𝐶 ) ) ) ) ↔ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑁 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) ) ) )
32		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝐶 ) = ∅
33	32	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ∅ ↦ 𝐶 ) = ∅ )
34	33	oveq2d	⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ∅ ) )
35		eqid	⊢ ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
36	35	gsum0	⊢ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ∅ ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
37	36	a1i	⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ∅ ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
38	34 37	eqtrd	⊢ ( 𝜑 → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
39	38	fveq2d	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ) )
40	1	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
41		eqid	⊢ ( Poly₁ ‘ 𝑅 ) = ( Poly₁ ‘ 𝑅 )
42		eqid	⊢ ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) = ( algSc ‘ ( Poly₁ ‘ 𝑅 ) )
43		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
44		eqid	⊢ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) = ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) )
45		eqid	⊢ ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) )
46	44 45	ringidval	⊢ ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
47	46	eqcomi	⊢ ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( 1_r ‘ ( Poly₁ ‘ 𝑅 ) )
48	41 42 43 47	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
49	40 48	syl	⊢ ( 𝜑 → ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
50	49	eqcomd	⊢ ( 𝜑 → ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) )
51	50	fveq2d	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ) )
52		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
53	52 43	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
54	40 53	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
55	1	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
56		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
57	55 56	syl	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
58		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
59	43 58	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1_r ‘ 𝑅 ) ≠ ( 0_g ‘ 𝑅 ) )
60	57 59	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) ≠ ( 0_g ‘ 𝑅 ) )
61		eqid	⊢ ( deg₁ ‘ 𝑅 ) = ( deg₁ ‘ 𝑅 )
62	61 41 52 42 58	deg1scl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1_r ‘ 𝑅 ) ≠ ( 0_g ‘ 𝑅 ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ) = 0 )
63	40 54 60 62	syl3anc	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ) = 0 )
64	51 63	eqtrd	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( 0_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ) = 0 )
65	39 64	eqtrd	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = 0 )
66		sum0	⊢ Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = 0
67	66	eqcomi	⊢ 0 = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) )
68	67	a1i	⊢ ( 𝜑 → 0 = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
69	65 68	eqtrd	⊢ ( 𝜑 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
70		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
71	70	leidd	⊢ ( 𝜑 → 0 ≤ 0 )
72	65	eqcomd	⊢ ( 𝜑 → 0 = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) )
73	71 72	breqtrd	⊢ ( 𝜑 → 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) )
74	69 73	jca	⊢ ( 𝜑 → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ∅ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ∅ ↦ 𝐶 ) ) ) ) )
75		nfcv	⊢ Ⅎ 𝑦 𝐶
76		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
77		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
78	75 76 77	cbvmpt	⊢ ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) = ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
79	78	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) = ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
80	79	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
81	80	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) )
82		eqid	⊢ ( Base ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
83		eqid	⊢ ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
84		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
85	1 84	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
86	85	simpld	⊢ ( 𝜑 → 𝑅 ∈ CRing )
87	41	ply1crng	⊢ ( 𝑅 ∈ CRing → ( Poly₁ ‘ 𝑅 ) ∈ CRing )
88	86 87	syl	⊢ ( 𝜑 → ( Poly₁ ‘ 𝑅 ) ∈ CRing )
89	44	crngmgp	⊢ ( ( Poly₁ ‘ 𝑅 ) ∈ CRing → ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ∈ CMnd )
90	88 89	syl	⊢ ( 𝜑 → ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ∈ CMnd )
91	90	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ∈ CMnd )
92	91	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ∈ CMnd )
93	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑁 ∈ Fin )
94		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑏 ⊆ 𝑁 )
95	93 94	ssfid	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑏 ∈ Fin )
96	94	sselda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑦 ∈ 𝑁 )
97		r19.26	⊢ ( ∀ 𝑥 ∈ 𝑁 ( 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
98	97	biimpi	⊢ ( ∀ 𝑥 ∈ 𝑁 ( 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
99	3 98	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
100	99	simpld	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
101	100	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
102		rspcsbela	⊢ ( ( 𝑦 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
103	96 101 102	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
104		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
105	44 104	mgpbas	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
106	103 105	eleqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
107		eldifi	⊢ ( 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) → 𝑐 ∈ 𝑁 )
108	107	adantl	⊢ ( ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) → 𝑐 ∈ 𝑁 )
109	108	adantl	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑐 ∈ 𝑁 )
110	109	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑐 ∈ 𝑁 )
111		eldifn	⊢ ( 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) → ¬ 𝑐 ∈ 𝑏 )
112	111	adantl	⊢ ( ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) → ¬ 𝑐 ∈ 𝑏 )
113	112	adantl	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ¬ 𝑐 ∈ 𝑏 )
114	113	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ¬ 𝑐 ∈ 𝑏 )
115	100	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
116		rspcsbela	⊢ ( ( 𝑐 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
117	110 115 116	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
118	117 105	eleqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
119		csbeq1	⊢ ( 𝑦 = 𝑐 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝑐 / 𝑥 ⦌ 𝐶 )
120	82 83 92 95 106 110 114 118 119	gsumunsn	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) = ( ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) )
121	120	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
122		eqid	⊢ ( ._r ‘ ( Poly₁ ‘ 𝑅 ) ) = ( ._r ‘ ( Poly₁ ‘ 𝑅 ) )
123	44 122	mgpplusg	⊢ ( ._r ‘ ( Poly₁ ‘ 𝑅 ) ) = ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
124	123	eqcomi	⊢ ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) = ( ._r ‘ ( Poly₁ ‘ 𝑅 ) )
125		eqid	⊢ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) = ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) )
126	55	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑅 ∈ Domn )
127	126	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑅 ∈ Domn )
128	103	ralrimiva	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ∀ 𝑦 ∈ 𝑏 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
129	105 92 95 128	gsummptcl	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
130	41	ply1idom	⊢ ( 𝑅 ∈ IDomn → ( Poly₁ ‘ 𝑅 ) ∈ IDomn )
131	1 130	syl	⊢ ( 𝜑 → ( Poly₁ ‘ 𝑅 ) ∈ IDomn )
132	131	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( Poly₁ ‘ 𝑅 ) ∈ IDomn )
133	132	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( Poly₁ ‘ 𝑅 ) ∈ IDomn )
134	99	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
135	134	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
136		rspcsbnea	⊢ ( ( 𝑦 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
137	96 135 136	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
138	44 133 95 103 137	idomnnzgmulnz	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
139	134	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
140		rspcsbnea	⊢ ( ( 𝑐 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
141	110 139 140	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
142	61 41 104 124 125 127 129 138 117 141	deg1mul	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
143	75 76 77	cbvmpt	⊢ ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
144	143	eqcomi	⊢ ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝑏 ↦ 𝐶 )
145	144	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) )
146	145	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) )
147	146	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) )
148	147	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
149		simpl	⊢ ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
150	149	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
151	150	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
152		nfv	⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) )
153		nfcv	⊢ Ⅎ 𝑛 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) )
154	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑁 ∈ Fin )
155		simprl	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑏 ⊆ 𝑁 )
156	154 155	ssfid	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑏 ∈ Fin )
157	75 76 77	cbvmpt	⊢ ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
158	157	fveq1i	⊢ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) = ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 )
159	158	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) = ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 ) )
160	159	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 ) ) )
161		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
162		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) ∧ 𝑦 = 𝑛 ) → 𝑦 = 𝑛 )
163	162	csbeq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) ∧ 𝑦 = 𝑛 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝑛 / 𝑥 ⦌ 𝐶 )
164	155	sselda	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → 𝑛 ∈ 𝑁 )
165	100	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
166	165	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
167		rspcsbela	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
168	164 166 167	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
169	161 163 164 168	fvmptd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 ) = ⦋ 𝑛 / 𝑥 ⦌ 𝐶 )
170	169	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ) )
171	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑅 ∈ Ring )
172	171	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → 𝑅 ∈ Ring )
173	134	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
174		rspcsbnea	⊢ ( ( 𝑛 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
175	164 173 174	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
176	61 41 125 104	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ) ∈ ℕ₀ )
177	172 168 175 176	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑛 / 𝑥 ⦌ 𝐶 ) ∈ ℕ₀ )
178	170 177	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑦 ∈ 𝑁 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ‘ 𝑛 ) ) ∈ ℕ₀ )
179	160 178	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∈ ℕ₀ )
180	179	nn0cnd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑛 ∈ 𝑏 ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∈ ℂ )
181		2fveq3	⊢ ( 𝑛 = 𝑐 → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) )
182	109 165 116	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
183		eqid	⊢ ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) = ( 𝑥 ∈ 𝑁 ↦ 𝐶 )
184	183	fvmpts	⊢ ( ( 𝑐 ∈ 𝑁 ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) = ⦋ 𝑐 / 𝑥 ⦌ 𝐶 )
185	109 182 184	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) = ⦋ 𝑐 / 𝑥 ⦌ 𝐶 )
186	185	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) )
187	108 134 140	syl2anr	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
188	61 41 125 104	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ∈ ℕ₀ )
189	171 182 187 188	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ∈ ℕ₀ )
190	186 189	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) ∈ ℕ₀ )
191	190	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) ∈ ℂ )
192	152 153 156 109 113 180 181 191	fsumsplitsn	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) ) )
193	192	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) ) )
194	185	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) = ⦋ 𝑐 / 𝑥 ⦌ 𝐶 )
195	194	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) = ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) )
196	195	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑐 ) ) ) = ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
197	193 196	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) )
198	197	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
199	151 198	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
200	148 199	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) + ( ( deg₁ ‘ 𝑅 ) ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
201	142 200	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ( +_g ‘ ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ) ⦋ 𝑐 / 𝑥 ⦌ 𝐶 ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
202	121 201	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
203	81 202	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) )
204	171	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 𝑅 ∈ Ring )
205	110	snssd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → { 𝑐 } ⊆ 𝑁 )
206	94 205	unssd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝑁 )
207	93 206	ssfid	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ∈ Fin )
208	165	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
209		ssralv	⊢ ( ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝑁 → ( ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
210	206 209	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
211	208 210	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ∀ 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
212	105 92 207 211	gsummptcl	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
213	78	oveq2i	⊢ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
214	213	a1i	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) = ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
215	109	snssd	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → { 𝑐 } ⊆ 𝑁 )
216	155 215	unssd	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ⊆ 𝑁 )
217	154 216	ssfid	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( 𝑏 ∪ { 𝑐 } ) ∈ Fin )
218	216	sselda	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → 𝑦 ∈ 𝑁 )
219	165	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
220	218 219 102	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
221	134	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ∀ 𝑥 ∈ 𝑁 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
222	218 221 136	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
223	44 132 217 220 222	idomnnzgmulnz	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
224	214 223	eqnetrd	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
225	224	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
226	61 41 125 104	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ∈ ℕ₀ )
227	204 212 225 226	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ∈ ℕ₀ )
228	227	nn0ge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) )
229	203 228	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ) )
230	229	ex	⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑏 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑏 ↦ 𝐶 ) ) ) ) → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ ( 𝑏 ∪ { 𝑐 } ) ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝐶 ) ) ) ) ) )
231	10 17 24 31 74 230 2	findcard2d	⊢ ( 𝜑 → ( ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) = Σ 𝑛 ∈ 𝑁 ( ( deg₁ ‘ 𝑅 ) ‘ ( ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ‘ 𝑛 ) ) ∧ 0 ≤ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( mulGrp ‘ ( Poly₁ ‘ 𝑅 ) ) Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝐶 ) ) ) ) )

Metamath Proof Explorer

Theorem deg1gprod

Proof