Theorem imasvscaval

Description: The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasvscaf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasvscaf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasvscaf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasvscaf.r	$$⊢\phi \to R\in Z$$
	imasvscaf.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
	imasvscaf.k	$$⊢K={\mathrm{Base}}_G$$
	imasvscaf.q	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	imasvscaf.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
	imasvscaf.e	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\to \left(F\left(a\right)=F\left(q\right)\to F\left(p\underset{\dot{}}{·}a\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
Assertion	imasvscaval	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to X\underset{\dot{}}{\bullet }F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasvscaf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasvscaf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasvscaf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
4		imasvscaf.r	$$⊢\phi \to R\in Z$$
5		imasvscaf.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
6		imasvscaf.k	$$⊢K={\mathrm{Base}}_G$$
7		imasvscaf.q	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
8		imasvscaf.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
9		imasvscaf.e	$$⊢\left(\phi \wedge \left(p\in K\wedge a\in V\wedge q\in V\right)\right)\to \left(F\left(a\right)=F\left(q\right)\to F\left(p\underset{\dot{}}{·}a\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
10	1 2 3 4 5 6 7 8 9	imasvscafn	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$
11		fnfun	$$⊢\underset{\dot{}}{\bullet }Fn\left(K\times B\right)\to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
12	10 11	syl	$$⊢\phi \to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
13	12	3ad2ant1	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to \mathrm{Fun}\underset{\dot{}}{\bullet }$$
14		eqidd	$$⊢q=Y\to K=K$$
15		fveq2	$$⊢q=Y\to F\left(q\right)=F\left(Y\right)$$
16	15	sneqd	$$⊢q=Y\to \left\{F\left(q\right)\right\}=\left\{F\left(Y\right)\right\}$$
17		oveq2	$$⊢q=Y\to p\underset{\dot{}}{·}q=p\underset{\dot{}}{·}Y$$
18	17	fveq2d	$$⊢q=Y\to F\left(p\underset{\dot{}}{·}q\right)=F\left(p\underset{\dot{}}{·}Y\right)$$
19	14 16 18	mpoeq123dv	$$⊢q=Y\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)=\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)$$
20	19	ssiun2s	$$⊢Y\in V\to \left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\subseteq \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
21	20	3ad2ant3	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to \left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\subseteq \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
22	1 2 3 4 5 6 7 8	imasvsca	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
23	22	3ad2ant1	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to \underset{\dot{}}{\bullet }=\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
24	21 23	sseqtrrd	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to \left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\subseteq \underset{\dot{}}{\bullet }$$
25		simp2	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to X\in K$$
26		fvex	$$⊢F\left(Y\right)\in \mathrm{V}$$
27	26	snid	$$⊢F\left(Y\right)\in \left\{F\left(Y\right)\right\}$$
28		opelxpi	$$⊢\left(X\in K\wedge F\left(Y\right)\in \left\{F\left(Y\right)\right\}\right)\to ⟨X,F\left(Y\right)⟩\in \left(K\times \left\{F\left(Y\right)\right\}\right)$$
29	25 27 28	sylancl	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to ⟨X,F\left(Y\right)⟩\in \left(K\times \left\{F\left(Y\right)\right\}\right)$$
30		eqid	$$⊢\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)=\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)$$
31		fvex	$$⊢F\left(p\underset{\dot{}}{·}Y\right)\in \mathrm{V}$$
32	30 31	dmmpo	$$⊢\mathrm{dom}\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)=K\times \left\{F\left(Y\right)\right\}$$
33	29 32	eleqtrrdi	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to ⟨X,F\left(Y\right)⟩\in \mathrm{dom}\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)$$
34		funssfv	$$⊢\left(\mathrm{Fun}\underset{\dot{}}{\bullet }\wedge \left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\subseteq \underset{\dot{}}{\bullet }\wedge ⟨X,F\left(Y\right)⟩\in \mathrm{dom}\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\right)\to \underset{\dot{}}{\bullet }\left(⟨X,F\left(Y\right)⟩\right)=\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\left(⟨X,F\left(Y\right)⟩\right)$$
35	13 24 33 34	syl3anc	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to \underset{\dot{}}{\bullet }\left(⟨X,F\left(Y\right)⟩\right)=\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\left(⟨X,F\left(Y\right)⟩\right)$$
36		df-ov	$$⊢X\underset{\dot{}}{\bullet }F\left(Y\right)=\underset{\dot{}}{\bullet }\left(⟨X,F\left(Y\right)⟩\right)$$
37		df-ov	$$⊢X\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)F\left(Y\right)=\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)\left(⟨X,F\left(Y\right)⟩\right)$$
38	35 36 37	3eqtr4g	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to X\underset{\dot{}}{\bullet }F\left(Y\right)=X\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)F\left(Y\right)$$
39		fvoveq1	$$⊢p=X\to F\left(p\underset{\dot{}}{·}Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
40		eqidd	$$⊢x=F\left(Y\right)\to F\left(X\underset{\dot{}}{·}Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
41		fvex	$$⊢F\left(X\underset{\dot{}}{·}Y\right)\in \mathrm{V}$$
42	39 40 30 41	ovmpo	$$⊢\left(X\in K\wedge F\left(Y\right)\in \left\{F\left(Y\right)\right\}\right)\to X\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
43	25 27 42	sylancl	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to X\left(p\in K,x\in \left\{F\left(Y\right)\right\}⟼F\left(p\underset{\dot{}}{·}Y\right)\right)F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
44	38 43	eqtrd	$$⊢\left(\phi \wedge X\in K\wedge Y\in V\right)\to X\underset{\dot{}}{\bullet }F\left(Y\right)=F\left(X\underset{\dot{}}{·}Y\right)$$