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	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
	xpsval.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	xpsval.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
	xpsval.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	xpsval.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	xpsval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
	xpsval.k	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
	xpsval.u	⊢ 𝑈 = ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
Assertion	xpsrnbas	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		xpsval.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2		xpsval.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
3		xpsval.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
4		xpsval.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		xpsval.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
6		xpsval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
7		xpsval.k	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
8		xpsval.u	⊢ 𝑈 = ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
9		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
10	7	fvexi	⊢ 𝐺 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐺 ∈ V )
12		2on	⊢ 2o ∈ On
13	12	a1i	⊢ ( 𝜑 → 2o ∈ On )
14		fnpr2o	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
15	4 5 14	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
16	8 9 11 13 15	prdsbas2	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = X 𝑘 ∈ 2o ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
17		fvprif	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
18	17	3expia	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑘 ∈ 2o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) )
19	4 5 18	syl2anc	⊢ ( 𝜑 → ( 𝑘 ∈ 2o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) )
20	19	imp	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) = if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
21	20	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) )
22		ifeq12	⊢ ( ( 𝑋 = ( Base ‘ 𝑅 ) ∧ 𝑌 = ( Base ‘ 𝑆 ) ) → if ( 𝑘 = ∅ , 𝑋 , 𝑌 ) = if ( 𝑘 = ∅ , ( Base ‘ 𝑅 ) , ( Base ‘ 𝑆 ) ) )
23	2 3 22	mp2an	⊢ if ( 𝑘 = ∅ , 𝑋 , 𝑌 ) = if ( 𝑘 = ∅ , ( Base ‘ 𝑅 ) , ( Base ‘ 𝑆 ) )
24		fvif	⊢ ( Base ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) ) = if ( 𝑘 = ∅ , ( Base ‘ 𝑅 ) , ( Base ‘ 𝑆 ) )
25	23 24	eqtr4i	⊢ if ( 𝑘 = ∅ , 𝑋 , 𝑌 ) = ( Base ‘ if ( 𝑘 = ∅ , 𝑅 , 𝑆 ) )
26	21 25	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = if ( 𝑘 = ∅ , 𝑋 , 𝑌 ) )
27	26	ixpeq2dva	⊢ ( 𝜑 → X 𝑘 ∈ 2o ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝑋 , 𝑌 ) )
28	6	xpsfrn	⊢ ran 𝐹 = X 𝑘 ∈ 2o if ( 𝑘 = ∅ , 𝑋 , 𝑌 )
29	27 28	eqtr4di	⊢ ( 𝜑 → X 𝑘 ∈ 2o ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ran 𝐹 )
30	16 29	eqtr2d	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑈 ) )