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

Metamath Proof Explorer

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

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 4 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
10 5 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
11 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
12 11 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝑋 )
13 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
14 13 3 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝑌 )
15 mpoeq12 ⊢ ( ( ( Base ‘ 𝑟 ) = 𝑋 ∧ ( Base ‘ 𝑠 ) = 𝑌 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
16 12 14 15 syl2an ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
17 16 6 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = 𝐹 )
18 17 cnveqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ◡ 𝐹 )
19 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Scalar ‘ 𝑟 ) = ( Scalar ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Scalar ‘ 𝑟 ) = ( Scalar ‘ 𝑅 ) )
21 20 7 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Scalar ‘ 𝑟 ) = 𝐺 )
22 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑟 = 𝑅 )
23 22 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⟨ ∅ , 𝑟 ⟩ = ⟨ ∅ , 𝑅 ⟩ )
24 simpr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
25 24 opeq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⟨ 1o , 𝑠 ⟩ = ⟨ 1o , 𝑆 ⟩ )
26 23 25 preq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } = { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
27 21 26 oveq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) = ( 𝐺 Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
28 27 8 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) = 𝑈 )
29 18 28 oveq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) ) = ( ◡ 𝐹 “s 𝑈 ) )
30 df-xps ⊢ ×s = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) ) )
31 ovex ⊢ ( ◡ 𝐹 “s 𝑈 ) ∈ V
32 29 30 31 ovmpoa ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 ×s 𝑆 ) = ( ◡ 𝐹 “s 𝑈 ) )
33 9 10 32 syl2anc ⊢ ( 𝜑 → ( 𝑅 ×s 𝑆 ) = ( ◡ 𝐹 “s 𝑈 ) )
34 1 33 eqtrid ⊢ ( 𝜑 → 𝑇 = ( ◡ 𝐹 “s 𝑈 ) )