coe1tm

Description: Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	coe1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
	coe1tm.k	$⊢ K = {Base}_{R}$
	coe1tm.p	$⊢ P = {Poly}_{1} (R)$
	coe1tm.x	$⊢ X = {var}_{1} (R)$
	coe1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	coe1tm.n	$⊢ N = {mulGrp}_{P}$
	coe1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
Assertion	coe1tm	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = (x \in ℕ_{0} ⟼ if (x = D, C, \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	$⊢ \underset{˙}{0} = 0_{R}$
2		coe1tm.k	$⊢ K = {Base}_{R}$
3		coe1tm.p	$⊢ P = {Poly}_{1} (R)$
4		coe1tm.x	$⊢ X = {var}_{1} (R)$
5		coe1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		coe1tm.n	$⊢ N = {mulGrp}_{P}$
7		coe1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
8		eqid	$⊢ {Base}_{P} = {Base}_{P}$
9	2 3 4 5 6 7 8	ply1tmcl	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in {Base}_{P}$
10		eqid	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X))$
11		eqid	$⊢ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) = (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
12	10 8 3 11	coe1fval2	$⊢ C \underset{˙}{\cdot} (D \underset{˙}{\times} X) \in {Base}_{P} \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
13	9 12	syl	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
14		fconst6g	$⊢ x \in ℕ_{0} \to (1_{𝑜} \times \{x\}) : 1_{𝑜} ⟶ ℕ_{0}$
15		nn0ex	$⊢ ℕ_{0} \in V$
16		1oex	$⊢ 1_{𝑜} \in V$
17	15 16	elmap	$⊢ 1_{𝑜} \times \{x\} \in ({ℕ_{0}}^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{x\}) : 1_{𝑜} ⟶ ℕ_{0}$
18	14 17	sylibr	$⊢ x \in ℕ_{0} \to 1_{𝑜} \times \{x\} \in ({ℕ_{0}}^{1_{𝑜}})$
19	18	adantl	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to 1_{𝑜} \times \{x\} \in ({ℕ_{0}}^{1_{𝑜}})$
20		eqidd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) = (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\})$
21		eqid	$⊢ \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
22	6 8	mgpbas	$⊢ {Base}_{P} = {Base}_{N}$
23	22	a1i	$⊢ R \in Ring \to {Base}_{P} = {Base}_{N}$
24		eqid	$⊢ {mulGrp}_{(1_{𝑜} mPoly R)} = {mulGrp}_{(1_{𝑜} mPoly R)}$
25	3 8	ply1bas	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
26	24 25	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
27	26	a1i	$⊢ R \in Ring \to {Base}_{P} = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
28		ssv	$⊢ {Base}_{P} \subseteq V$
29	28	a1i	$⊢ R \in Ring \to {Base}_{P} \subseteq V$
30		ovexd	$⊢ (R \in Ring \land (x \in V \land y \in V)) \to x +_{N} y \in V$
31		eqid	$⊢ \cdot_{P} = \cdot_{P}$
32	6 31	mgpplusg	$⊢ \cdot_{P} = +_{N}$
33		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
34	3 33 31	ply1mulr	$⊢ \cdot_{P} = \cdot_{(1_{𝑜} mPoly R)}$
35	24 34	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
36	32 35	eqtr3i	$⊢ +_{N} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
37	36	a1i	$⊢ R \in Ring \to +_{N} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
38	37	oveqdr	$⊢ (R \in Ring \land (x \in V \land y \in V)) \to x +_{N} y = x +_{{mulGrp}_{(1_{𝑜} mPoly R)}} y$
39	7 21 23 27 29 30 38	mulgpropd	$⊢ R \in Ring \to \underset{˙}{\times} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
40	39	3ad2ant1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to \underset{˙}{\times} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
41		eqidd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D = D$
42	4	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
43	42	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to X = (1_{𝑜} mVar R) (\emptyset)$
44	40 41 43	oveq123d	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D \underset{˙}{\times} X = D \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
45	44	oveq2d	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) = C \underset{˙}{\cdot} (D \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset))$
46		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{a \in ({ℕ_{0}}^{1_{𝑜}}) \| a^{-1} [ℕ] \in Fin\}$
47		eqid	$⊢ 1_{R} = 1_{R}$
48		1on	$⊢ 1_{𝑜} \in On$
49	48	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to 1_{𝑜} \in On$
50		eqid	$⊢ 1_{𝑜} mVar R = 1_{𝑜} mVar R$
51		simp1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to R \in Ring$
52		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
53	52	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to \emptyset \in 1_{𝑜}$
54		simp3	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D \in ℕ_{0}$
55	33 46 1 47 49 24 21 50 51 53 54	mplcoe3	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (y \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), 1_{R}, \underset{˙}{0})) = D \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset)$
56	55	oveq2d	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (y \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), 1_{R}, \underset{˙}{0})) = C \underset{˙}{\cdot} (D \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}} (1_{𝑜} mVar R) (\emptyset))$
57	3 33 5	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
58		elsni	$⊢ b \in \{\emptyset\} \to b = \emptyset$
59		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
60	58 59	eleq2s	$⊢ b \in 1_{𝑜} \to b = \emptyset$
61	60	iftrued	$⊢ b \in 1_{𝑜} \to if (b = \emptyset, D, 0) = D$
62	61	adantl	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land b \in 1_{𝑜}) \to if (b = \emptyset, D, 0) = D$
63	62	mpteq2dva	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) = (b \in 1_{𝑜} ⟼ D)$
64		fconstmpt	$⊢ 1_{𝑜} \times \{D\} = (b \in 1_{𝑜} ⟼ D)$
65	63 64	eqtr4di	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) = 1_{𝑜} \times \{D\}$
66		fconst6g	$⊢ D \in ℕ_{0} \to (1_{𝑜} \times \{D\}) : 1_{𝑜} ⟶ ℕ_{0}$
67	15 16	elmap	$⊢ 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{D\}) : 1_{𝑜} ⟶ ℕ_{0}$
68	66 67	sylibr	$⊢ D \in ℕ_{0} \to 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}})$
69	68	3ad2ant3	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}})$
70	65 69	eqeltrd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) \in ({ℕ_{0}}^{1_{𝑜}})$
71		simp2	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \in K$
72	33 57 46 47 1 2 49 51 70 71	mplmon2	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (y \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), 1_{R}, \underset{˙}{0})) = (y \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0}))$
73	45 56 72	3eqtr2d	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \underset{˙}{\cdot} (D \underset{˙}{\times} X) = (y \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0}))$
74		eqeq1	$⊢ y = 1_{𝑜} \times \{x\} \to (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) \leftrightarrow 1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)))$
75	74	ifbid	$⊢ y = 1_{𝑜} \times \{x\} \to if (y = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0}) = if (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0})$
76	19 20 73 75	fmptco	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) \circ (x \in ℕ_{0} ⟼ 1_{𝑜} \times \{x\}) = (x \in ℕ_{0} ⟼ if (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0}))$
77	65	adantr	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) = 1_{𝑜} \times \{D\}$
78	77	eqeq2d	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) \leftrightarrow 1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\})$
79		fveq1	$⊢ 1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\} \to (1_{𝑜} \times \{x\}) (\emptyset) = (1_{𝑜} \times \{D\}) (\emptyset)$
80		vex	$⊢ x \in V$
81	80	fvconst2	$⊢ \emptyset \in 1_{𝑜} \to (1_{𝑜} \times \{x\}) (\emptyset) = x$
82	52 81	mp1i	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\}) (\emptyset) = x$
83		simpl3	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to D \in ℕ_{0}$
84		fvconst2g	$⊢ (D \in ℕ_{0} \land \emptyset \in 1_{𝑜}) \to (1_{𝑜} \times \{D\}) (\emptyset) = D$
85	83 52 84	sylancl	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{D\}) (\emptyset) = D$
86	82 85	eqeq12d	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to ((1_{𝑜} \times \{x\}) (\emptyset) = (1_{𝑜} \times \{D\}) (\emptyset) \leftrightarrow x = D)$
87	79 86	imbitrid	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\} \to x = D)$
88		sneq	$⊢ x = D \to \{x\} = \{D\}$
89	88	xpeq2d	$⊢ x = D \to 1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\}$
90	87 89	impbid1	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\} \leftrightarrow x = D)$
91	78 90	bitrd	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) \leftrightarrow x = D)$
92	91	ifbid	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to if (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0}) = if (x = D, C, \underset{˙}{0})$
93	92	mpteq2dva	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (x \in ℕ_{0} ⟼ if (1_{𝑜} \times \{x\} = (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)), C, \underset{˙}{0})) = (x \in ℕ_{0} ⟼ if (x = D, C, \underset{˙}{0}))$
94	13 76 93	3eqtrd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to {coe}_{1} (C \underset{˙}{\cdot} (D \underset{˙}{\times} X)) = (x \in ℕ_{0} ⟼ if (x = D, C, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem coe1tm

Proof