Theorem xpsrnbas

Description: The indexed structure product that appears in xpsval has the same base as the target of the function F . (Contributed by Mario Carneiro, 15-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	xpsrnbas	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_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		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
10	7	fvexi	$$⊢G\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to G\in \mathrm{V}$$
12		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
13	12	a1i	$$⊢\phi \to 2_{𝑜}\in \mathrm{On}$$
14		fnpr2o	$$⊢\left(R\in V\wedge S\in W\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}$$
15	4 5 14	syl2anc	$$⊢\phi \to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}Fn{2}_{𝑜}$$
16	8 9 11 13 15	prdsbas2	$$⊢\phi \to {\mathrm{Base}}_U=\underset{k\in 2_{𝑜}}{⨉}{\mathrm{Base}}_{\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)}$$
17		fvprif	$$⊢\left(R\in V\wedge S\in W\wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)$$
18	17	3expia	$$⊢\left(R\in V\wedge S\in W\right)\to \left(k\in 2_{𝑜}\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)\right)$$
19	4 5 18	syl2anc	$$⊢\phi \to \left(k\in 2_{𝑜}\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)\right)$$
20	19	imp	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to \left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)=if\left(k=\varnothing ,R,S\right)$$
21	20	fveq2d	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)}={\mathrm{Base}}_{if\left(k=\varnothing ,R,S\right)}$$
22		ifeq12	$$⊢\left(X={\mathrm{Base}}_R\wedge Y={\mathrm{Base}}_S\right)\to if\left(k=\varnothing ,X,Y\right)=if\left(k=\varnothing ,{\mathrm{Base}}_R,{\mathrm{Base}}_S\right)$$
23	2 3 22	mp2an	$$⊢if\left(k=\varnothing ,X,Y\right)=if\left(k=\varnothing ,{\mathrm{Base}}_R,{\mathrm{Base}}_S\right)$$
24		fvif	$$⊢{\mathrm{Base}}_{if\left(k=\varnothing ,R,S\right)}=if\left(k=\varnothing ,{\mathrm{Base}}_R,{\mathrm{Base}}_S\right)$$
25	23 24	eqtr4i	$$⊢if\left(k=\varnothing ,X,Y\right)={\mathrm{Base}}_{if\left(k=\varnothing ,R,S\right)}$$
26	21 25	syl6eqr	$$⊢\left(\phi \wedge k\in 2_{𝑜}\right)\to {\mathrm{Base}}_{\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)}=if\left(k=\varnothing ,X,Y\right)$$
27	26	ixpeq2dva	$$⊢\phi \to \underset{k\in 2_{𝑜}}{⨉}{\mathrm{Base}}_{\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)}=\underset{k\in 2_{𝑜}}{⨉}if\left(k=\varnothing ,X,Y\right)$$
28	6	xpsfrn	$$⊢\mathrm{ran}F=\underset{k\in 2_{𝑜}}{⨉}if\left(k=\varnothing ,X,Y\right)$$
29	27 28	syl6eqr	$$⊢\phi \to \underset{k\in 2_{𝑜}}{⨉}{\mathrm{Base}}_{\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\left(k\right)}=\mathrm{ran}F$$
30	16 29	eqtr2d	$$⊢\phi \to \mathrm{ran}F={\mathrm{Base}}_U$$