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		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
26	3 25 8	ply1bas	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
27	24 26	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
28	27	a1i	$⊢ R \in Ring \to {Base}_{P} = {Base}_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
29		ssv	$⊢ {Base}_{P} \subseteq V$
30	29	a1i	$⊢ R \in Ring \to {Base}_{P} \subseteq V$
31		ovexd	$⊢ (R \in Ring \land (x \in V \land y \in V)) \to x +_{N} y \in V$
32		eqid	$⊢ \cdot_{P} = \cdot_{P}$
33	6 32	mgpplusg	$⊢ \cdot_{P} = +_{N}$
34		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
35	3 34 32	ply1mulr	$⊢ \cdot_{P} = \cdot_{(1_{𝑜} mPoly R)}$
36	24 35	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
37	33 36	eqtr3i	$⊢ +_{N} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
38	37	a1i	$⊢ R \in Ring \to +_{N} = +_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
39	38	oveqdr	$⊢ (R \in Ring \land (x \in V \land y \in V)) \to x +_{N} y = x +_{{mulGrp}_{(1_{𝑜} mPoly R)}} y$
40	7 21 23 28 30 31 39	mulgpropd	$⊢ R \in Ring \to \underset{˙}{\times} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
41	40	3ad2ant1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to \underset{˙}{\times} = \cdot_{{mulGrp}_{(1_{𝑜} mPoly R)}}$
42		eqidd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D = D$
43	4	vr1val	$⊢ X = (1_{𝑜} mVar R) (\emptyset)$
44	43	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to X = (1_{𝑜} mVar R) (\emptyset)$
45	41 42 44	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)$
46	45	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))$
47		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{a \in ({ℕ_{0}}^{1_{𝑜}}) \| a^{-1} [ℕ] \in Fin\}$
48		eqid	$⊢ 1_{R} = 1_{R}$
49		1on	$⊢ 1_{𝑜} \in On$
50	49	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to 1_{𝑜} \in On$
51		eqid	$⊢ 1_{𝑜} mVar R = 1_{𝑜} mVar R$
52		simp1	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to R \in Ring$
53		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
54	53	a1i	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to \emptyset \in 1_{𝑜}$
55		simp3	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to D \in ℕ_{0}$
56	34 47 1 48 50 24 21 51 52 54 55	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)$
57	56	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))$
58	3 34 5	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
59		elsni	$⊢ b \in \{\emptyset\} \to b = \emptyset$
60		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
61	59 60	eleq2s	$⊢ b \in 1_{𝑜} \to b = \emptyset$
62	61	iftrued	$⊢ b \in 1_{𝑜} \to if (b = \emptyset, D, 0) = D$
63	62	adantl	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land b \in 1_{𝑜}) \to if (b = \emptyset, D, 0) = D$
64	63	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)$
65		fconstmpt	$⊢ 1_{𝑜} \times \{D\} = (b \in 1_{𝑜} ⟼ D)$
66	64 65	syl6eqr	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) = 1_{𝑜} \times \{D\}$
67		fconst6g	$⊢ D \in ℕ_{0} \to (1_{𝑜} \times \{D\}) : 1_{𝑜} ⟶ ℕ_{0}$
68	15 16	elmap	$⊢ 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{D\}) : 1_{𝑜} ⟶ ℕ_{0}$
69	67 68	sylibr	$⊢ D \in ℕ_{0} \to 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}})$
70	69	3ad2ant3	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to 1_{𝑜} \times \{D\} \in ({ℕ_{0}}^{1_{𝑜}})$
71	66 70	eqeltrd	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to (b \in 1_{𝑜} ⟼ if (b = \emptyset, D, 0)) \in ({ℕ_{0}}^{1_{𝑜}})$
72		simp2	$⊢ (R \in Ring \land C \in K \land D \in ℕ_{0}) \to C \in K$
73	34 58 47 48 1 2 50 52 71 72	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}))$
74	46 57 73	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}))$
75		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)))$
76	75	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})$
77	19 20 74 76	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}))$
78	66	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\}$
79	78	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\})$
80		fveq1	$⊢ 1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\} \to (1_{𝑜} \times \{x\}) (\emptyset) = (1_{𝑜} \times \{D\}) (\emptyset)$
81		vex	$⊢ x \in V$
82	81	fvconst2	$⊢ \emptyset \in 1_{𝑜} \to (1_{𝑜} \times \{x\}) (\emptyset) = x$
83	53 82	mp1i	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{x\}) (\emptyset) = x$
84		simpl3	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to D \in ℕ_{0}$
85		fvconst2g	$⊢ (D \in ℕ_{0} \land \emptyset \in 1_{𝑜}) \to (1_{𝑜} \times \{D\}) (\emptyset) = D$
86	84 53 85	sylancl	$⊢ ((R \in Ring \land C \in K \land D \in ℕ_{0}) \land x \in ℕ_{0}) \to (1_{𝑜} \times \{D\}) (\emptyset) = D$
87	83 86	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)$
88	80 87	syl5ib	$⊢ ((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)$
89		sneq	$⊢ x = D \to \{x\} = \{D\}$
90	89	xpeq2d	$⊢ x = D \to 1_{𝑜} \times \{x\} = 1_{𝑜} \times \{D\}$
91	88 90	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)$
92	79 91	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)$
93	92	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})$
94	93	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}))$
95	13 77 94	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