Theorem xpssca

Description: Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpssca.t	$$⊢T=R{\times }_{𝑠}S$$
	xpssca.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
	xpssca.1	$$⊢\phi \to R\in V$$
	xpssca.2	$$⊢\phi \to S\in W$$
Assertion	xpssca	$$⊢\phi \to G=\mathrm{Scalar}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpssca.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpssca.g	$$⊢G=\mathrm{Scalar}\left(R\right)$$
3		xpssca.1	$$⊢\phi \to R\in V$$
4		xpssca.2	$$⊢\phi \to S\in W$$
5		eqid	$$⊢G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}=G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
6	2	fvexi	$$⊢G\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to G\in \mathrm{V}$$
8		prex	$$⊢\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
10	5 7 9	prdssca	$$⊢\phi \to G=\mathrm{Scalar}\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
13		eqid	$$⊢\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
14	1 11 12 3 4 13 2 5	xpsval	$$⊢\phi \to T={\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
15	1 11 12 3 4 13 2 5	xpsrnbas	$$⊢\phi \to \mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)={\mathrm{Base}}_{\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)}$$
16	13	xpsff1o2	$$⊢\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):{\mathrm{Base}}_R\times {\mathrm{Base}}_S\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
17		f1ocnv	$$⊢\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):{\mathrm{Base}}_R\times {\mathrm{Base}}_S\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\to {\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\times {\mathrm{Base}}_S$$
18	16 17	mp1i	$$⊢\phi \to {\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\times {\mathrm{Base}}_S$$
19		f1ofo	$$⊢{\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}{\mathrm{Base}}_R\times {\mathrm{Base}}_S\to {\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}{\mathrm{Base}}_R\times {\mathrm{Base}}_S$$
20	18 19	syl	$$⊢\phi \to {\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}{\mathrm{Base}}_R\times {\mathrm{Base}}_S$$
21		ovexd	$$⊢\phi \to G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
22		eqid	$$⊢\mathrm{Scalar}\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)=\mathrm{Scalar}\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
23	14 15 20 21 22	imassca	$$⊢\phi \to \mathrm{Scalar}\left(G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)=\mathrm{Scalar}\left(T\right)$$
24	10 23	eqtrd	$$⊢\phi \to G=\mathrm{Scalar}\left(T\right)$$