Theorem asclfval

Description: Function value of the algebra scalar lifting function. (Contributed by Mario Carneiro, 8-Mar-2015)

	Ref	Expression
Hypotheses	asclfval.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclfval.k	$$⊢K={\mathrm{Base}}_F$$
	asclfval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	asclfval.o	$$⊢\underset{\dot{}}{1}=1_W$$
Assertion	asclfval	$$⊢A=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclfval.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclfval.k	$$⊢K={\mathrm{Base}}_F$$
4		asclfval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		asclfval.o	$$⊢\underset{\dot{}}{1}=1_W$$
6		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
7	6 2	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=F$$
8	7	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_F$$
9	8 3	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=K$$
10		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
11	10 4	eqtr4di	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
12		eqidd	$$⊢w=W\to x=x$$
13		fveq2	$$⊢w=W\to 1_w=1_W$$
14	13 5	eqtr4di	$$⊢w=W\to 1_w=\underset{\dot{}}{1}$$
15	11 12 14	oveq123d	$$⊢w=W\to x{\cdot }_w{1}_w=x\underset{\dot{}}{·}\underset{\dot{}}{1}$$
16	9 15	mpteq12dv	$$⊢w=W\to \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
17		df-ascl	$$⊢\mathrm{algSc}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}⟼x{\cdot }_w{1}_w\right)\right)$$
18	16 17 3	mptfvmpt	$$⊢W\in \mathrm{V}\to \mathrm{algSc}\left(W\right)=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
19		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{algSc}\left(W\right)=\varnothing$$
20		mpt0	$$⊢\left(x\in \varnothing ⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=\varnothing$$
21	19 20	eqtr4di	$$⊢\neg W\in \mathrm{V}\to \mathrm{algSc}\left(W\right)=\left(x\in \varnothing ⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
22		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{Scalar}\left(W\right)=\varnothing$$
23	2 22	eqtrid	$$⊢\neg W\in \mathrm{V}\to F=\varnothing$$
24	23	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_F={\mathrm{Base}}_{\varnothing }$$
25		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
26	24 25	eqtr4di	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_F=\varnothing$$
27	3 26	eqtrid	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
28	27	mpteq1d	$$⊢\neg W\in \mathrm{V}\to \left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=\left(x\in \varnothing ⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
29	21 28	eqtr4d	$$⊢\neg W\in \mathrm{V}\to \mathrm{algSc}\left(W\right)=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
30	18 29	pm2.61i	$$⊢\mathrm{algSc}\left(W\right)=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
31	1 30	eqtri	$$⊢A=\left(x\in K⟼x\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$