Theorem evls1fval 22362

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

Hypotheses

Ref	Expression
evls1fval.q	⊢ 𝑄 = (𝑆 evalSub1 𝑅)
evls1fval.e	⊢ 𝐸 = (1o evalSub 𝑆)
evls1fval.b	⊢ 𝐵 = (Base‘𝑆)

Assertion

Ref	Expression
evls1fval	⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))

Distinct variable group:   𝑥,𝐵,𝑦

Allowed substitution hints:   𝑄(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem evls1fval

Dummy variables 𝑏 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evls1fval.q	. 2 ⊢ 𝑄 = (𝑆 evalSub1 𝑅)
2		elex 3474	. . . 4 ⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V)
3	2	adantr 484	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑆 ∈ V)
4		simpr 488	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑅 ∈ 𝒫 𝐵)
5		ovex 7425	. . . . . 6 ⊢ (𝐵 ↑m (𝐵 ↑m 1o)) ∈ V
6	5	mptex 7203	. . . . 5 ⊢ (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∈ V
7		fvex 6876	. . . . 5 ⊢ (𝐸‘𝑅) ∈ V
8	6, 7	coex 7907	. . . 4 ⊢ ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V
9	8	a1i 11	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V)
10		fveq2 6863	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
11	10	adantr 484	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = (Base‘𝑆))
12		evls1fval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑆)
13	11, 12	eqtr4di 2814	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = 𝐵)
14	13	csbeq1d 3856	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
15	12	fvexi 6877	. . . . . . 7 ⊢ 𝐵 ∈ V
16	15	a1i 11	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝐵 ∈ V)
17		id 22	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → 𝑏 = 𝐵)
18		oveq1 7399	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑏 ↑m 1o) = (𝐵 ↑m 1o))
19	17, 18	oveq12d 7410	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑏 ↑m (𝑏 ↑m 1o)) = (𝐵 ↑m (𝐵 ↑m 1o)))
20		mpteq1 5188	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})) = (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))
21	20	coeq2d 5832	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))) = (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))))
22	19, 21	mpteq12dv 5186	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) = (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))))
23	22	coeq1d 5831	. . . . . . 7 ⊢ (𝑏 = 𝐵 → ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
24	23	adantl 485	. . . . . 6 ⊢ (((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) ∧ 𝑏 = 𝐵) → ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
25	16, 24	csbied 3888	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
26		oveq2 7400	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (1o evalSub 𝑠) = (1o evalSub 𝑆))
27		evls1fval.e	. . . . . . . . 9 ⊢ 𝐸 = (1o evalSub 𝑆)
28	26, 27	eqtr4di 2814	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (1o evalSub 𝑠) = 𝐸)
29	28	adantr 484	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (1o evalSub 𝑠) = 𝐸)
30		simpr 488	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
31	29, 30	fveq12d 6870	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((1o evalSub 𝑠)‘𝑟) = (𝐸‘𝑅))
32	31	coeq2d 5832	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
33	14, 25, 32	3eqtrd 2800	. . . 4 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
34	10, 12	eqtr4di 2814	. . . . 5 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
35	34	pweqd 4571	. . . 4 ⊢ (𝑠 = 𝑆 → 𝒫 (Base‘𝑠) = 𝒫 𝐵)
36		df-evls1 22358	. . . 4 ⊢ evalSub1 = (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o evalSub 𝑠)‘𝑟)))
37	33, 35, 36	ovmpox 7545	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 𝐵 ∧ ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
38	3, 4, 9, 37	syl3anc 1389	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))
39	1, 38	eqtrid 2808	1 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ⦋csb 3852  𝒫 cpw 4554  {csn 4581   ↦ cmpt 5180   × cxp 5643   ∘ ccom 5649  ‘cfv 6517  (class class class)co 7392  1_oc1o 8425   ↑_m cmap 8803  Basecbs 17228   evalSub ces 22105   evalSub₁ ces1 22356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-evls1 22358

This theorem is referenced by:  evls1val  22363  evls1rhm  22365  evls1sca  22366  evl1fval1lem  22373