Theorem scaffval

Description: The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	scaffval.b	$$⊢B={\mathrm{Base}}_W$$
	scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	scaffval.k	$$⊢K={\mathrm{Base}}_F$$
	scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	scaffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	$$⊢B={\mathrm{Base}}_W$$
2		scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		scaffval.k	$$⊢K={\mathrm{Base}}_F$$
4		scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
5		scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
7	6 2	syl6eqr	$$⊢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	syl6eqr	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=K$$
10		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
11	10 1	syl6eqr	$$⊢w=W\to {\mathrm{Base}}_w=B$$
12		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
13	12 5	syl6eqr	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
14	13	oveqd	$$⊢w=W\to x{\cdot }_{w}y=x\underset{\dot{}}{·}y$$
15	9 11 14	mpoeq123dv	$$⊢w=W\to \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},y\in {\mathrm{Base}}_w⟼x{\cdot }_{w}y\right)=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
16		df-scaf	$$⊢{\cdot }_{\mathrm{𝑠𝑓}}=\left(w\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)},y\in {\mathrm{Base}}_w⟼x{\cdot }_{w}y\right)\right)$$
17	3	fvexi	$$⊢K\in \mathrm{V}$$
18	1	fvexi	$$⊢B\in \mathrm{V}$$
19	5	fvexi	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
20	19	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{·}\in \mathrm{V}$$
21		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
22	20 21	unex	$$⊢\mathrm{ran}\underset{\dot{}}{·}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
23		df-ov	$$⊢x\underset{\dot{}}{·}y=\underset{\dot{}}{·}\left(⟨x,y⟩\right)$$
24		fvrn0	$$⊢\underset{\dot{}}{·}\left(⟨x,y⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{·}\cup \left\{\varnothing \right\}\right)$$
25	23 24	eqeltri	$$⊢x\underset{\dot{}}{·}y\in \left(\mathrm{ran}\underset{\dot{}}{·}\cup \left\{\varnothing \right\}\right)$$
26	25	rgen2w	$$⊢\forall x\in K\forall y\in Bx\underset{\dot{}}{·}y\in \left(\mathrm{ran}\underset{\dot{}}{·}\cup \left\{\varnothing \right\}\right)$$
27	17 18 22 26	mpoexw	$$⊢\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)\in \mathrm{V}$$
28	15 16 27	fvmpt	$$⊢W\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
29		fvprc	$$⊢\neg W\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)=\varnothing$$
30		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
31	1 30	syl5eq	$$⊢\neg W\in \mathrm{V}\to B=\varnothing$$
32	31	olcd	$$⊢\neg W\in \mathrm{V}\to \left(K=\varnothing \vee B=\varnothing \right)$$
33		0mpo0	$$⊢\left(K=\varnothing \vee B=\varnothing \right)\to \left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)=\varnothing$$
34	32 33	syl	$$⊢\neg W\in \mathrm{V}\to \left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)=\varnothing$$
35	29 34	eqtr4d	$$⊢\neg W\in \mathrm{V}\to {\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
36	28 35	pm2.61i	$$⊢{\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
37	4 36	eqtri	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$