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	syl5eq	⊢ ( 𝜑 → 𝑇 = ( ◡ 𝐹 “s 𝑈 ) )