ply1coe - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ply1coe		Structured version Visualization version GIF version

Theorem ply1coe 21811

Description: Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by AV, 7-Oct-2019.)

**Hypotheses**
Ref	Expression
ply1coe.p	⊢ 𝑃 = (Poly₁‘𝑅)
ply1coe.x	⊢ 𝑋 = (var₁‘𝑅)
ply1coe.b	⊢ 𝐵 = (Base‘𝑃)
ply1coe.n	⊢ · = ( ·_𝑠 ‘𝑃)
ply1coe.m	⊢ 𝑀 = (mulGrp‘𝑃)
ply1coe.e	⊢ ↑ = (._g‘𝑀)
ply1coe.a	⊢ 𝐴 = (coe₁‘𝐾)

**Assertion**
Ref	Expression
ply1coe	⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝑘,𝐾 𝑘,𝑋 ↑ ,𝑘 𝑅,𝑘 · ,𝑘 𝑃,𝑘 Allowed substitution hint: 𝑀(𝑘)

Proof of Theorem ply1coe Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2732	. . 3 ⊢ (1_o mPoly 𝑅) = (1_o mPoly 𝑅)
2		psr1baslem 21700	. . 3 ⊢ (ℕ₀ ↑_m 1_o) = {𝑑 ∈ (ℕ₀ ↑_m 1_o) ∣ (^◡𝑑 “ ℕ) ∈ Fin}
3		eqid 2732	. . 3 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
4		eqid 2732	. . 3 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
5		1onn 8635	. . . 4 ⊢ 1_o ∈ ω
6	5	a1i 11	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 1_o ∈ ω)
7		ply1coe.p	. . . 4 ⊢ 𝑃 = (Poly₁‘𝑅)
8		eqid 2732	. . . 4 ⊢ (PwSer₁‘𝑅) = (PwSer₁‘𝑅)
9		ply1coe.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
10	7, 8, 9	ply1bas 21710	. . 3 ⊢ 𝐵 = (Base‘(1_o mPoly 𝑅))
11		ply1coe.n	. . . 4 ⊢ · = ( ·_𝑠 ‘𝑃)
12	7, 1, 11	ply1vsca 21739	. . 3 ⊢ · = ( ·_𝑠 ‘(1_o mPoly 𝑅))
13		simpl 483	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑅 ∈ Ring)
14		simpr 485	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 ∈ 𝐵)
15	1, 2, 3, 4, 6, 10, 12, 13, 14	mplcoe1 21583	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))))))
16		ply1coe.a	. . . . . . 7 ⊢ 𝐴 = (coe₁‘𝐾)
17	16	fvcoe1 21722	. . . . . 6 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
18	17	adantll 712	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝐾‘𝑎) = (𝐴‘(𝑎‘∅)))
19	5	a1i 11	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 1_o ∈ ω)
20		eqid 2732	. . . . . . 7 ⊢ (mulGrp‘(1_o mPoly 𝑅)) = (mulGrp‘(1_o mPoly 𝑅))
21		eqid 2732	. . . . . . 7 ⊢ (._g‘(mulGrp‘(1_o mPoly 𝑅))) = (._g‘(mulGrp‘(1_o mPoly 𝑅)))
22		eqid 2732	. . . . . . 7 ⊢ (1_o mVar 𝑅) = (1_o mVar 𝑅)
23		simpll 765	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑅 ∈ Ring)
24		simpr 485	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑎 ∈ (ℕ₀ ↑_m 1_o))
25		eqidd 2733	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
26		0ex 5306	. . . . . . . . . . 11 ⊢ ∅ ∈ V
27		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ((1_o mVar 𝑅)‘𝑏) = ((1_o mVar 𝑅)‘∅))
28	27	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
29	27	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
30	28, 29	eqeq12d 2748	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ((((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅))))
31	26, 30	ralsn 4684	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
32	25, 31	sylibr 233	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
33		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((1_o mVar 𝑅)‘𝑥) = ((1_o mVar 𝑅)‘∅))
34	33	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)))
35	33	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
36	34, 35	eqeq12d 2748	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ((((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏))))
37	36	ralbidv 3177	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏))))
38	26, 37	ralsn 4684	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘∅)) = (((1_o mVar 𝑅)‘∅)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
39	32, 38	sylibr 233	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
40		df1o2 8469	. . . . . . . . 9 ⊢ 1_o = {∅}
41	40	raleqi 3323	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
42	40, 41	raleqbii 3338	. . . . . . . 8 ⊢ (∀𝑥 ∈ 1_o ∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)) ↔ ∀𝑥 ∈ {∅}∀𝑏 ∈ {∅} (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
43	39, 42	sylibr 233	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∀𝑥 ∈ 1_o ∀𝑏 ∈ 1_o (((1_o mVar 𝑅)‘𝑏)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑥)) = (((1_o mVar 𝑅)‘𝑥)(+_g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑏)))
44	1, 2, 3, 4, 19, 20, 21, 22, 23, 24, 43	mplcoe5 21586	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))) = ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))))
45	40	mpteq1i 5243	. . . . . . . 8 ⊢ (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐))) = (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))
46	45	oveq2i 7416	. . . . . . 7 ⊢ ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐))))
47	1	mplring 21569	. . . . . . . . . . 11 ⊢ ((1_o ∈ ω ∧ 𝑅 ∈ Ring) → (1_o mPoly 𝑅) ∈ Ring)
48	5, 47	mpan 688	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (1_o mPoly 𝑅) ∈ Ring)
49	20	ringmgp 20055	. . . . . . . . . 10 ⊢ ((1_o mPoly 𝑅) ∈ Ring → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
50	48, 49	syl 17	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
51	50	ad2antrr 724	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd)
52	26	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ∅ ∈ V)
53		ply1coe.e	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘𝑀)
54	20, 10	mgpbas 19987	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘(mulGrp‘(1_o mPoly 𝑅)))
55	54	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘(mulGrp‘(1_o mPoly 𝑅))))
56		ply1coe.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (mulGrp‘𝑃)
57	56, 9	mgpbas 19987	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑀)
58	57	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 = (Base‘𝑀))
59		ssv 4005	. . . . . . . . . . . . 13 ⊢ 𝐵 ⊆ V
60	59	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐵 ⊆ V)
61		ovexd 7440	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) ∈ V)
62		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑃) = (._r‘𝑃)
63	7, 1, 62	ply1mulr 21740	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝑃) = (._r‘(1_o mPoly 𝑅))
64	20, 63	mgpplusg 19985	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑃) = (+_g‘(mulGrp‘(1_o mPoly 𝑅)))
65	56, 62	mgpplusg 19985	. . . . . . . . . . . . . . 15 ⊢ (._r‘𝑃) = (+_g‘𝑀)
66	64, 65	eqtr3i 2762	. . . . . . . . . . . . . 14 ⊢ (+_g‘(mulGrp‘(1_o mPoly 𝑅))) = (+_g‘𝑀)
67	66	oveqi 7418	. . . . . . . . . . . . 13 ⊢ (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) = (𝑎(+_g‘𝑀)𝑏)
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → (𝑎(+_g‘(mulGrp‘(1_o mPoly 𝑅)))𝑏) = (𝑎(+_g‘𝑀)𝑏))
69	21, 53, 55, 58, 60, 61, 68	mulgpropd 18990	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (._g‘(mulGrp‘(1_o mPoly 𝑅))) = ↑ )
70	69	oveqd 7422	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
71	70	adantr 481	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) = ((𝑎‘∅) ↑ 𝑋))
72	7	ply1ring 21761	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
73	56	ringmgp 20055	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑀 ∈ Mnd)
74	72, 73	syl 17	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
75	74	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑀 ∈ Mnd)
76		elmapi 8839	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) → 𝑎:1_o⟶ℕ₀)
77		0lt1o 8500	. . . . . . . . . . . 12 ⊢ ∅ ∈ 1_o
78		ffvelcdm 7080	. . . . . . . . . . . 12 ⊢ ((𝑎:1_o⟶ℕ₀ ∧ ∅ ∈ 1_o) → (𝑎‘∅) ∈ ℕ₀)
79	76, 77, 78	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) → (𝑎‘∅) ∈ ℕ₀)
80	79	adantl 482	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑎‘∅) ∈ ℕ₀)
81		ply1coe.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (var₁‘𝑅)
82	81, 7, 9	vr1cl 21732	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵)
83	82	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → 𝑋 ∈ 𝐵)
84	57, 53, 75, 80, 83	mulgnn0cld 18969	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅) ↑ 𝑋) ∈ 𝐵)
85	71, 84	eqeltrd 2833	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) ∈ 𝐵)
86		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → (𝑎‘𝑐) = (𝑎‘∅))
87		fveq2 6888	. . . . . . . . . . 11 ⊢ (𝑐 = ∅ → ((1_o mVar 𝑅)‘𝑐) = ((1_o mVar 𝑅)‘∅))
88	81	vr1val 21707	. . . . . . . . . . 11 ⊢ 𝑋 = ((1_o mVar 𝑅)‘∅)
89	87, 88	eqtr4di 2790	. . . . . . . . . 10 ⊢ (𝑐 = ∅ → ((1_o mVar 𝑅)‘𝑐) = 𝑋)
90	86, 89	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
91	54, 90	gsumsn 19816	. . . . . . . 8 ⊢ (((mulGrp‘(1_o mPoly 𝑅)) ∈ Mnd ∧ ∅ ∈ V ∧ ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋) ∈ 𝐵) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
92	51, 52, 85, 91	syl3anc 1371	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ {∅} ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
93	46, 92	eqtrid 2784	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((mulGrp‘(1_o mPoly 𝑅)) Σ_g (𝑐 ∈ 1_o ↦ ((𝑎‘𝑐)(._g‘(mulGrp‘(1_o mPoly 𝑅)))((1_o mVar 𝑅)‘𝑐)))) = ((𝑎‘∅)(._g‘(mulGrp‘(1_o mPoly 𝑅)))𝑋))
94	44, 93, 71	3eqtrd 2776	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))) = ((𝑎‘∅) ↑ 𝑋))
95	18, 94	oveq12d 7423	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ₀ ↑_m 1_o)) → ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
96	95	mpteq2dva 5247	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅))))) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
97	96	oveq2d 7421	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐾‘𝑎) · (𝑏 ∈ (ℕ₀ ↑_m 1_o) ↦ if(𝑏 = 𝑎, (1_r‘𝑅), (0_g‘𝑅)))))) = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
98		nn0ex 12474	. . . . . 6 ⊢ ℕ₀ ∈ V
99	98	mptex 7221	. . . . 5 ⊢ (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V
100	99	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∈ V)
101	7	fvexi 6902	. . . . 5 ⊢ 𝑃 ∈ V
102	101	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝑃 ∈ V)
103		ovexd 7440	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ V)
104	9, 10	eqtr3i 2762	. . . . 5 ⊢ (Base‘𝑃) = (Base‘(1_o mPoly 𝑅))
105	104	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (Base‘𝑃) = (Base‘(1_o mPoly 𝑅)))
106		eqid 2732	. . . . . 6 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
107	7, 1, 106	ply1plusg 21738	. . . . 5 ⊢ (+_g‘𝑃) = (+_g‘(1_o mPoly 𝑅))
108	107	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (+_g‘𝑃) = (+_g‘(1_o mPoly 𝑅)))
109	100, 102, 103, 105, 108	gsumpropd 18593	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1_o mPoly 𝑅) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
110		eqid 2732	. . . . 5 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
111	1, 7, 110	ply1mpl0 21768	. . . 4 ⊢ (0_g‘𝑃) = (0_g‘(1_o mPoly 𝑅))
112	1	mpllmod 21568	. . . . . 6 ⊢ ((1_o ∈ ω ∧ 𝑅 ∈ Ring) → (1_o mPoly 𝑅) ∈ LMod)
113	5, 13, 112	sylancr 587	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ LMod)
114		lmodcmn 20512	. . . . 5 ⊢ ((1_o mPoly 𝑅) ∈ LMod → (1_o mPoly 𝑅) ∈ CMnd)
115	113, 114	syl 17	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (1_o mPoly 𝑅) ∈ CMnd)
116	98	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ℕ₀ ∈ V)
117	7	ply1lmod 21765	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
118	117	ad2antrr 724	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑃 ∈ LMod)
119		eqid 2732	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
120	16, 9, 7, 119	coe1f 21726	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝐵 → 𝐴:ℕ₀⟶(Base‘𝑅))
121	120	adantl 482	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐴:ℕ₀⟶(Base‘𝑅))
122	121	ffvelcdmda 7083	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ (Base‘𝑅))
123	7	ply1sca 21766	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
124	123	eqcomd 2738	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
125	124	ad2antrr 724	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (Scalar‘𝑃) = 𝑅)
126	125	fveq2d 6892	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
127	122, 126	eleqtrrd 2836	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
128	74	ad2antrr 724	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑀 ∈ Mnd)
129		simpr 485	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
130	82	ad2antrr 724	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑋 ∈ 𝐵)
131	57, 53, 128, 129, 130	mulgnn0cld 18969	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ 𝑋) ∈ 𝐵)
132		eqid 2732	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
133		eqid 2732	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
134	9, 132, 11, 133	lmodvscl 20481	. . . . . 6 ⊢ ((𝑃 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑘 ↑ 𝑋) ∈ 𝐵) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
135	118, 127, 131, 134	syl3anc 1371	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) ∈ 𝐵)
136	135	fmpttd 7111	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))):ℕ₀⟶𝐵)
137	7, 81, 9, 11, 56, 53, 16	ply1coefsupp 21810	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) finSupp (0_g‘𝑃))
138		eqid 2732	. . . . . 6 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅))
139	40, 98, 26, 138	mapsnf1o2 8884	. . . . 5 ⊢ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)):(ℕ₀ ↑_m 1_o)–1-1-onto→ℕ₀
140	139	a1i 11	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)):(ℕ₀ ↑_m 1_o)–1-1-onto→ℕ₀)
141	10, 111, 115, 116, 136, 137, 140	gsumf1o 19778	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))) = ((1_o mPoly 𝑅) Σ_g ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))))
142		eqidd 2733	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))
143		eqidd 2733	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) = (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))))
144		fveq2 6888	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝐴‘𝑘) = (𝐴‘(𝑎‘∅)))
145		oveq1 7412	. . . . . 6 ⊢ (𝑘 = (𝑎‘∅) → (𝑘 ↑ 𝑋) = ((𝑎‘∅) ↑ 𝑋))
146	144, 145	oveq12d 7423	. . . . 5 ⊢ (𝑘 = (𝑎‘∅) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)) = ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))
147	80, 142, 143, 146	fmptco 7123	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅))) = (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋))))
148	147	oveq2d 7421	. . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g ((𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋))) ∘ (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ (𝑎‘∅)))) = ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))))
149	109, 141, 148	3eqtrrd 2777	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → ((1_o mPoly 𝑅) Σ_g (𝑎 ∈ (ℕ₀ ↑_m 1_o) ↦ ((𝐴‘(𝑎‘∅)) · ((𝑎‘∅) ↑ 𝑋)))) = (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))
150	15, 97, 149	3eqtrd 2776	1 ⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵) → 𝐾 = (𝑃 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑋)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 ⊆ wss 3947 ∅c0 4321 ifcif 4527 {csn 4627 ↦ cmpt 5230 ∘ ccom 5679 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ωcom 7851 1_oc1o 8455 ↑_m cmap 8816 ℕ₀cn0 12468 Basecbs 17140 +_gcplusg 17193 ._rcmulr 17194 Scalarcsca 17196 ·_𝑠 cvsca 17197 0_gc0g 17381 Σ_g cgsu 17382 Mndcmnd 18621 ._gcmg 18944 CMndccmn 19642 mulGrpcmgp 19981 1_rcur 19998 Ringcrg 20049 LModclmod 20463 mVar cmvr 21449 mPoly cmpl 21450 PwSer₁cps1 21690 var₁cv1 21691 Poly₁cpl1 21692 coe₁cco1 21693

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-ofr 7667 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-sup 9433 df-oi 9501 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-fzo 13624 df-seq 13963 df-hash 14287 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-plusg 17206 df-mulr 17207 df-sca 17209 df-vsca 17210 df-ip 17211 df-tset 17212 df-ple 17213 df-ds 17215 df-hom 17217 df-cco 17218 df-0g 17383 df-gsum 17384 df-prds 17389 df-pws 17391 df-mre 17526 df-mrc 17527 df-acs 17529 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-mhm 18667 df-submnd 18668 df-grp 18818 df-minusg 18819 df-sbg 18820 df-mulg 18945 df-subg 18997 df-ghm 19084 df-cntz 19175 df-cmn 19644 df-abl 19645 df-mgp 19982 df-ur 19999 df-srg 20003 df-ring 20051 df-subrg 20353 df-lmod 20465 df-lss 20535 df-psr 21453 df-mvr 21454 df-mpl 21455 df-opsr 21457 df-psr1 21695 df-vr1 21696 df-ply1 21697 df-coe1 21698

This theorem is referenced by: eqcoe1ply1eq 21812 pmatcollpw1lem2 22268 mp2pm2mp 22304 plypf1 25717 evls1fpws 32634 ply1degltdimlem 32695

W3C validator