Theorem xpsval

Description: Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Jim Kingdon, 25-Sep-2023)

	Ref	Expression
Hypotheses	xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsval.x	$$⊢X={\mathrm{Base}}_R$$
	xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsval.1	$$⊢\phi \to R\in V$$
	xpsval.2	$$⊢\phi \to S\in W$$
	xpsval.f	$$⊢F=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
	xpsval.k	$$⊢G=\mathrm{Scalar}\left(R\right)$$
	xpsval.u	$$⊢U=G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
Assertion	xpsval	$$⊢\phi \to T=F^{-1}{“}_{𝑠}U$$

Proof

Step	Hyp	Ref	Expression
1		xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsval.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsval.1	$$⊢\phi \to R\in V$$
5		xpsval.2	$$⊢\phi \to S\in W$$
6		xpsval.f	$$⊢F=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
7		xpsval.k	$$⊢G=\mathrm{Scalar}\left(R\right)$$
8		xpsval.u	$$⊢U=G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
9	4	elexd	$$⊢\phi \to R\in \mathrm{V}$$
10	5	elexd	$$⊢\phi \to S\in \mathrm{V}$$
11		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
12	11 2	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=X$$
13		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
14	13 3	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=Y$$
15		mpoeq12	$$⊢\left({\mathrm{Base}}_r=X\wedge {\mathrm{Base}}_s=Y\right)\to \left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
16	12 14 15	syl2an	$$⊢\left(r=R\wedge s=S\right)\to \left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
17	16 6	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=F$$
18	17	cnveqd	$$⊢\left(r=R\wedge s=S\right)\to {\left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}=F^{-1}$$
19		fveq2	$$⊢r=R\to \mathrm{Scalar}\left(r\right)=\mathrm{Scalar}\left(R\right)$$
20	19	adantr	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{Scalar}\left(r\right)=\mathrm{Scalar}\left(R\right)$$
21	20 7	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{Scalar}\left(r\right)=G$$
22		simpl	$$⊢\left(r=R\wedge s=S\right)\to r=R$$
23	22	opeq2d	$$⊢\left(r=R\wedge s=S\right)\to ⟨\varnothing ,r⟩=⟨\varnothing ,R⟩$$
24		simpr	$$⊢\left(r=R\wedge s=S\right)\to s=S$$
25	24	opeq2d	$$⊢\left(r=R\wedge s=S\right)\to ⟨1_{𝑜},s⟩=⟨1_{𝑜},S⟩$$
26	23 25	preq12d	$$⊢\left(r=R\wedge s=S\right)\to \left\{⟨\varnothing ,r⟩,⟨1_{𝑜},s⟩\right\}=\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
27	21 26	oveq12d	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left\{⟨\varnothing ,r⟩,⟨1_{𝑜},s⟩\right\}=G{⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
28	27 8	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to \mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left\{⟨\varnothing ,r⟩,⟨1_{𝑜},s⟩\right\}=U$$
29	18 28	oveq12d	$$⊢\left(r=R\wedge s=S\right)\to {\left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left\{⟨\varnothing ,r⟩,⟨1_{𝑜},s⟩\right\}\right)=F^{-1}{“}_{𝑠}U$$
30		df-xps	$$⊢{\times }_{𝑠}=\left(r\in \mathrm{V},s\in \mathrm{V}⟼{\left(x\in {\mathrm{Base}}_r,y\in {\mathrm{Base}}_s⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left(r\right){⨉}_{𝑠}\left\{⟨\varnothing ,r⟩,⟨1_{𝑜},s⟩\right\}\right)\right)$$
31		ovex	$$⊢F^{-1}{“}_{𝑠}U\in \mathrm{V}$$
32	29 30 31	ovmpoa	$$⊢\left(R\in \mathrm{V}\wedge S\in \mathrm{V}\right)\to R{\times }_{𝑠}S=F^{-1}{“}_{𝑠}U$$
33	9 10 32	syl2anc	$$⊢\phi \to R{\times }_{𝑠}S=F^{-1}{“}_{𝑠}U$$
34	1 33	syl5eq	$$⊢\phi \to T=F^{-1}{“}_{𝑠}U$$