evl1fval

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	evl1fval.o	$⊢ O = {eval}_{1} (R)$
	evl1fval.q	$⊢ Q = 1_{𝑜} eval R$
	evl1fval.b	$⊢ B = {Base}_{R}$
Assertion	evl1fval	$⊢ O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$

Proof

Step	Hyp	Ref	Expression
1		evl1fval.o	$⊢ O = {eval}_{1} (R)$
2		evl1fval.q	$⊢ Q = 1_{𝑜} eval R$
3		evl1fval.b	$⊢ B = {Base}_{R}$
4		fvexd	$⊢ r = R \to {Base}_{r} \in V$
5		id	$⊢ b = {Base}_{r} \to b = {Base}_{r}$
6		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
7	6 3	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
8	5 7	sylan9eqr	$⊢ (r = R \land b = {Base}_{r}) \to b = B$
9	8	oveq1d	$⊢ (r = R \land b = {Base}_{r}) \to b^{1_{𝑜}} = B^{1_{𝑜}}$
10	8 9	oveq12d	$⊢ (r = R \land b = {Base}_{r}) \to b^{(b^{1_{𝑜}})} = B^{(B^{1_{𝑜}})}$
11	8	mpteq1d	$⊢ (r = R \land b = {Base}_{r}) \to (y \in b ⟼ 1_{𝑜} \times \{y\}) = (y \in B ⟼ 1_{𝑜} \times \{y\})$
12	11	coeq2d	$⊢ (r = R \land b = {Base}_{r}) \to x \circ (y \in b ⟼ 1_{𝑜} \times \{y\}) = x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})$
13	10 12	mpteq12dv	$⊢ (r = R \land b = {Base}_{r}) \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\}))$
14		simpl	$⊢ (r = R \land b = {Base}_{r}) \to r = R$
15	14	oveq2d	$⊢ (r = R \land b = {Base}_{r}) \to 1_{𝑜} eval r = 1_{𝑜} eval R$
16	15 2	eqtr4di	$⊢ (r = R \land b = {Base}_{r}) \to 1_{𝑜} eval r = Q$
17	13 16	coeq12d	$⊢ (r = R \land b = {Base}_{r}) \to (x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
18	4 17	csbied	$⊢ r = R \to ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r)) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
19		df-evl1	$⊢ {eval}_{1} = (r \in V ⟼ ⦋ {Base}_{r} / b ⦌ ((x \in (b^{(b^{1_{𝑜}})}) ⟼ x \circ (y \in b ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval r)))$
20		ovex	$⊢ B^{(B^{1_{𝑜}})} \in V$
21	20	mptex	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in V$
22	2	ovexi	$⊢ Q \in V$
23	21 22	coex	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q \in V$
24	18 19 23	fvmpt	$⊢ R \in V \to {eval}_{1} (R) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
25	1 24	syl5eq	$⊢ R \in V \to O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
26		fvprc	$⊢ \neg R \in V \to {eval}_{1} (R) = \emptyset$
27	1 26	syl5eq	$⊢ \neg R \in V \to O = \emptyset$
28		co02	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ \emptyset = \emptyset$
29	27 28	eqtr4di	$⊢ \neg R \in V \to O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ \emptyset$
30		df-evl	$⊢ eval = (i \in V, r \in V ⟼ (i evalSub r) ({Base}_{r}))$
31	30	reldmmpo	$⊢ Rel dom eval$
32	31	ovprc2	$⊢ \neg R \in V \to 1_{𝑜} eval R = \emptyset$
33	2 32	syl5eq	$⊢ \neg R \in V \to Q = \emptyset$
34	33	coeq2d	$⊢ \neg R \in V \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ \emptyset$
35	29 34	eqtr4d	$⊢ \neg R \in V \to O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$
36	25 35	pm2.61i	$⊢ O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ Q$

Metamath Proof Explorer

Theorem evl1fval

Proof