Theorem imasvscaf

Description: The image structure's scalar multiplication is closed in the base set. (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)$$
	imasvscaf.c	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
Assertion	imasvscaf	$$⊢\phi \to \underset{\dot{}}{\bullet }:K\times B⟶B$$

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		imasvscaf.c	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
11	1 2 3 4 5 6 7 8 9	imasvscafn	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$
12	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)$$
13		fof	$$⊢F:V\underset{onto}{⟶}B\to F:V⟶B$$
14	3 13	syl	$$⊢\phi \to F:V⟶B$$
15	14	ffvelrnda	$$⊢\left(\phi \wedge p\underset{\dot{}}{·}q\in V\right)\to F\left(p\underset{\dot{}}{·}q\right)\in B$$
16	10 15	syldan	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to F\left(p\underset{\dot{}}{·}q\right)\in B$$
17	16	ralrimivw	$$⊢\left(\phi \wedge \left(p\in K\wedge q\in V\right)\right)\to \forall x\in \left\{F\left(q\right)\right\}F\left(p\underset{\dot{}}{·}q\right)\in B$$
18	17	anass1rs	$$⊢\left(\left(\phi \wedge q\in V\right)\wedge p\in K\right)\to \forall x\in \left\{F\left(q\right)\right\}F\left(p\underset{\dot{}}{·}q\right)\in B$$
19	18	ralrimiva	$$⊢\left(\phi \wedge q\in V\right)\to \forall p\in K\forall x\in \left\{F\left(q\right)\right\}F\left(p\underset{\dot{}}{·}q\right)\in B$$
20		eqid	$$⊢\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(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)$$
21	20	fmpo	$$⊢\forall p\in K\forall x\in \left\{F\left(q\right)\right\}F\left(p\underset{\dot{}}{·}q\right)\in B\leftrightarrow \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶B$$
22	19 21	sylib	$$⊢\left(\phi \wedge q\in V\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶B$$
23		fssxp	$$⊢\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right):K\times \left\{F\left(q\right)\right\}⟶B\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times \left\{F\left(q\right)\right\}\right)\times B$$
24	22 23	syl	$$⊢\left(\phi \wedge q\in V\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times \left\{F\left(q\right)\right\}\right)\times B$$
25	14	ffvelrnda	$$⊢\left(\phi \wedge q\in V\right)\to F\left(q\right)\in B$$
26	25	snssd	$$⊢\left(\phi \wedge q\in V\right)\to \left\{F\left(q\right)\right\}\subseteq B$$
27		xpss2	$$⊢\left\{F\left(q\right)\right\}\subseteq B\to K\times \left\{F\left(q\right)\right\}\subseteq K\times B$$
28		xpss1	$$⊢K\times \left\{F\left(q\right)\right\}\subseteq K\times B\to \left(K\times \left\{F\left(q\right)\right\}\right)\times B\subseteq \left(K\times B\right)\times B$$
29	26 27 28	3syl	$$⊢\left(\phi \wedge q\in V\right)\to \left(K\times \left\{F\left(q\right)\right\}\right)\times B\subseteq \left(K\times B\right)\times B$$
30	24 29	sstrd	$$⊢\left(\phi \wedge q\in V\right)\to \left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times B$$
31	30	ralrimiva	$$⊢\phi \to \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times B$$
32		iunss	$$⊢\bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times B\leftrightarrow \forall q\in V\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times B$$
33	31 32	sylibr	$$⊢\phi \to \bigcup _{q\in V}\left(p\in K,x\in \left\{F\left(q\right)\right\}⟼F\left(p\underset{\dot{}}{·}q\right)\right)\subseteq \left(K\times B\right)\times B$$
34	12 33	eqsstrd	$$⊢\phi \to \underset{\dot{}}{\bullet }\subseteq \left(K\times B\right)\times B$$
35		dff2	$$⊢\underset{\dot{}}{\bullet }:K\times B⟶B\leftrightarrow \left(\underset{\dot{}}{\bullet }Fn\left(K\times B\right)\wedge \underset{\dot{}}{\bullet }\subseteq \left(K\times B\right)\times B\right)$$
36	11 34 35	sylanbrc	$$⊢\phi \to \underset{\dot{}}{\bullet }:K\times B⟶B$$