This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑈 ) )