Theorem xpsval 16894

Description: Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)

Hypotheses

Ref	Expression
xpsval.t	⊢ 𝑇 = (𝑅 ×s 𝑆)
xpsval.x	⊢ 𝑋 = (Base‘𝑅)
xpsval.y	⊢ 𝑌 = (Base‘𝑆)
xpsval.1	⊢ (𝜑 → 𝑅 ∈ 𝑉)
xpsval.2	⊢ (𝜑 → 𝑆 ∈ 𝑊)
xpsval.f	⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
xpsval.k	⊢ 𝐺 = (Scalar‘𝑅)
xpsval.u	⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})

Assertion

Ref	Expression
xpsval	⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))

Distinct variable groups:   𝑥,𝑦   𝑥,𝑊   𝑥,𝑋,𝑦   𝑥,𝑅   𝑥,𝑌,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑅(𝑦)   𝑆(𝑥,𝑦)   𝑇(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑦)

Proof of Theorem xpsval

Dummy variables 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpsval.t	. 2 ⊢ 𝑇 = (𝑅 ×s 𝑆)
2		xpsval.1	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
3	2	elexd 3431	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
4		xpsval.2	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
5	4	elexd 3431	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
6		fveq2 6659	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
7		xpsval.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
8	6, 7	eqtr4di 2812	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋)
9		fveq2 6659	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10		xpsval.y	. . . . . . . . 9 ⊢ 𝑌 = (Base‘𝑆)
11	9, 10	eqtr4di 2812	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌)
12		mpoeq12 7222	. . . . . . . 8 ⊢ (((Base‘𝑟) = 𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
13	8, 11, 12	syl2an 599	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
14		xpsval.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
15	13, 14	eqtr4di 2812	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = 𝐹)
16	15	cnveqd 5716	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = ◡𝐹)
17		fveq2 6659	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅))
18	17	adantr 485	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅))
19		xpsval.k	. . . . . . . 8 ⊢ 𝐺 = (Scalar‘𝑅)
20	18, 19	eqtr4di 2812	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺)
21		simpl 487	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
22	21	opeq2d 4771	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨∅, 𝑟⟩ = ⟨∅, 𝑅⟩)
23		simpr 489	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
24	23	opeq2d 4771	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨1o, 𝑠⟩ = ⟨1o, 𝑆⟩)
25	22, 24	preq12d 4635	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩} = {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
26	20, 25	oveq12d 7169	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
27		xpsval.u	. . . . . 6 ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
28	26, 27	eqtr4di 2812	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = 𝑈)
29	16, 28	oveq12d 7169	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})) = (◡𝐹 “s 𝑈))
30		df-xps 16834	. . . 4 ⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31		ovex 7184	. . . 4 ⊢ (◡𝐹 “s 𝑈) ∈ V
32	29, 30, 31	ovmpoa 7301	. . 3 ⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
33	3, 5, 32	syl2anc 588	. 2 ⊢ (𝜑 → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
34	1, 33	syl5eq 2806	1 ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  Vcvv 3410  ∅c0 4226  {cpr 4525  ⟨cop 4529  ^◡ccnv 5524  ‘cfv 6336  (class class class)co 7151   ∈ cmpo 7153  1_oc1o 8106  Basecbs 16534  Scalarcsca 16619  X_scprds 16770   “_s cimas 16828   ×_s cxps 16830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-xps 16834

This theorem is referenced by:  xpsbas  16896  xpsadd  16898  xpsmul  16899  xpssca  16900  xpsvsca  16901  xpsless  16902  xpsle  16903  xpsmnd  18010  xpsgrp  18278  xpstps  22503  xpstopnlem2  22504  xpsdsfn  23072  xpsxmet  23075  xpsdsval  23076  xpsmet  23077  xpsxms  23229  xpsms  23230