evls1fval

Description: Value of the univariate polynomial evaluation map function. (Contributed by AV, 7-Sep-2019)

	Ref	Expression
Hypotheses	evls1fval.q	$⊢ Q = S {evalSub}_{1} R$
	evls1fval.e	$⊢ E = 1_{𝑜} evalSub S$
	evls1fval.b	$⊢ B = {Base}_{S}$
Assertion	evls1fval	$⊢ (S \in V \land R \in 𝒫 B) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$

Proof

Step	Hyp	Ref	Expression
1		evls1fval.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1fval.e	$⊢ E = 1_{𝑜} evalSub S$
3		evls1fval.b	$⊢ B = {Base}_{S}$
4		elex	$⊢ S \in V \to S \in V$
5	4	adantr	$⊢ (S \in V \land R \in 𝒫 B) \to S \in V$
6		simpr	$⊢ (S \in V \land R \in 𝒫 B) \to R \in 𝒫 B$
7		ovex	$⊢ B^{(B^{1_{𝑜}})} \in V$
8	7	mptex	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in V$
9		fvex	$⊢ E (R) \in V$
10	8 9	coex	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R) \in V$
11	10	a1i	$⊢ (S \in V \land R \in 𝒫 B) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R) \in V$
12		fveq2	$⊢ s = S \to {Base}_{s} = {Base}_{S}$
13	12	adantr	$⊢ (s = S \land r = R) \to {Base}_{s} = {Base}_{S}$
14	13 3	eqtr4di	$⊢ (s = S \land r = R) \to {Base}_{s} = B$
15	14	csbeq1d	$⊢ (s = S \land r = R) \to ⦋ {Base}_{s} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)) = ⦋ B / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r))$
16	3	fvexi	$⊢ B \in V$
17	16	a1i	$⊢ (s = S \land r = R) \to B \in V$
18		id	$⊢ b = B \to b = B$
19		oveq1	$⊢ b = B \to b^{1_{𝑜}} = B^{1_{𝑜}}$
20	18 19	oveq12d	$⊢ b = B \to b^{(b^{1_{𝑜}})} = B^{(B^{1_{𝑜}})}$
21		mpteq1	$⊢ b = B \to (y \in b ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
22	21	coeq2d	$⊢ b = B \to x \circ (y \in b ⟼ 1_{𝑜} \times \{y\}) = x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
23	20 22	mpteq12dv	$⊢ b = B \to (x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}))$
24	23	coeq1d	$⊢ b = B \to (x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)$
25	24	adantl	$⊢ ((s = S \land r = R) \land b = B) \to (x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)$
26	17 25	csbied	$⊢ (s = S \land r = R) \to ⦋ B / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)$
27		oveq2	$⊢ s = S \to 1_{𝑜} evalSub s = 1_{𝑜} evalSub S$
28	27 2	eqtr4di	$⊢ s = S \to 1_{𝑜} evalSub s = E$
29	28	adantr	$⊢ (s = S \land r = R) \to 1_{𝑜} evalSub s = E$
30		simpr	$⊢ (s = S \land r = R) \to r = R$
31	29 30	fveq12d	$⊢ (s = S \land r = R) \to (1_{𝑜} evalSub s) (r) = E (R)$
32	31	coeq2d	$⊢ (s = S \land r = R) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
33	15 26 32	3eqtrd	$⊢ (s = S \land r = R) \to ⦋ {Base}_{s} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
34	12 3	eqtr4di	$⊢ s = S \to {Base}_{s} = B$
35	34	pweqd	$⊢ s = S \to 𝒫 {Base}_{s} = 𝒫 B$
36		df-evls1	$⊢ {evalSub}_{1} = (s \in V, r \in 𝒫 {Base}_{s} ⟼ ⦋ {Base}_{s} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub s) (r)))$
37	33 35 36	ovmpox	$⊢ (S \in V \land R \in 𝒫 B \land (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R) \in V) \to S {evalSub}_{1} R = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
38	5 6 11 37	syl3anc	$⊢ (S \in V \land R \in 𝒫 B) \to S {evalSub}_{1} R = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$
39	1 38	syl5eq	$⊢ (S \in V \land R \in 𝒫 B) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ E (R)$

Metamath Proof Explorer

Theorem evls1fval

Proof