Theorem xpsval 17491

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 3464	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
4		xpsval.2	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
5	4	elexd 3464	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
6		fveq2 6834	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
7		xpsval.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
8	6, 7	eqtr4di 2789	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋)
9		fveq2 6834	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10		xpsval.y	. . . . . . . . 9 ⊢ 𝑌 = (Base‘𝑆)
11	9, 10	eqtr4di 2789	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌)
12		mpoeq12 7431	. . . . . . . 8 ⊢ (((Base‘𝑟) = 𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
13	8, 11, 12	syl2an 596	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
14		xpsval.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
15	13, 14	eqtr4di 2789	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = 𝐹)
16	15	cnveqd 5824	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = ◡𝐹)
17		fveq2 6834	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅))
18	17	adantr 480	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅))
19		xpsval.k	. . . . . . . 8 ⊢ 𝐺 = (Scalar‘𝑅)
20	18, 19	eqtr4di 2789	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺)
21		simpl 482	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
22	21	opeq2d 4836	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨∅, 𝑟⟩ = ⟨∅, 𝑅⟩)
23		simpr 484	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
24	23	opeq2d 4836	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨1o, 𝑠⟩ = ⟨1o, 𝑆⟩)
25	22, 24	preq12d 4698	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩} = {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
26	20, 25	oveq12d 7376	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
27		xpsval.u	. . . . . 6 ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
28	26, 27	eqtr4di 2789	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = 𝑈)
29	16, 28	oveq12d 7376	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})) = (◡𝐹 “s 𝑈))
30		df-xps 17431	. . . 4 ⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31		ovex 7391	. . . 4 ⊢ (◡𝐹 “s 𝑈) ∈ V
32	29, 30, 31	ovmpoa 7513	. . 3 ⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
33	3, 5, 32	syl2anc 584	. 2 ⊢ (𝜑 → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
34	1, 33	eqtrid 2783	1 ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  {cpr 4582  ⟨cop 4586  ^◡ccnv 5623  ‘cfv 6492  (class class class)co 7358   ∈ cmpo 7360  1_oc1o 8390  Basecbs 17136  Scalarcsca 17180  X_scprds 17365   “_s cimas 17425   ×_s cxps 17427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-xps 17431

This theorem is referenced by:  xpsbas  17493  xpsadd  17495  xpsmul  17496  xpssca  17497  xpsvsca  17498  xpsless  17499  xpsle  17500  xpsmnd  18702  xpsgrp  18989  xpsrngd  20114  xpsringd  20268  xpstps  23754  xpstopnlem2  23755  xpsdsfn  24321  xpsxmet  24324  xpsdsval  24325  xpsmet  24326  xpsxms  24478  xpsms  24479