Theorem xpsval 16676

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 3460	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
4		xpsval.2	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
5	4	elexd 3460	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
6		fveq2 6545	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
7		xpsval.x	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝑅)
8	6, 7	syl6eqr 2851	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋)
9		fveq2 6545	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10		xpsval.y	. . . . . . . . 9 ⊢ 𝑌 = (Base‘𝑆)
11	9, 10	syl6eqr 2851	. . . . . . . 8 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌)
12		mpoeq12 7092	. . . . . . . 8 ⊢ (((Base‘𝑟) = 𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
13	8, 11, 12	syl2an 595	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
14		xpsval.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
15	13, 14	syl6eqr 2851	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = 𝐹)
16	15	cnveqd 5639	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = ◡𝐹)
17		fveq2 6545	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅))
18	17	adantr 481	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅))
19		xpsval.k	. . . . . . . 8 ⊢ 𝐺 = (Scalar‘𝑅)
20	18, 19	syl6eqr 2851	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺)
21		simpl 483	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
22	21	opeq2d 4723	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨∅, 𝑟⟩ = ⟨∅, 𝑅⟩)
23		simpr 485	. . . . . . . . 9 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
24	23	opeq2d 4723	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ⟨1o, 𝑠⟩ = ⟨1o, 𝑆⟩)
25	22, 24	preq12d 4590	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩} = {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
26	20, 25	oveq12d 7041	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
27		xpsval.u	. . . . . 6 ⊢ 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
28	26, 27	syl6eqr 2851	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = 𝑈)
29	16, 28	oveq12d 7041	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})) = (◡𝐹 “s 𝑈))
30		df-xps 16616	. . . 4 ⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31		ovex 7055	. . . 4 ⊢ (◡𝐹 “s 𝑈) ∈ V
32	29, 30, 31	ovmpoa 7168	. . 3 ⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
33	3, 5, 32	syl2anc 584	. 2 ⊢ (𝜑 → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈))
34	1, 33	syl5eq 2845	1 ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525   ∈ wcel 2083  Vcvv 3440  ∅c0 4217  {cpr 4480  ⟨cop 4484  ^◡ccnv 5449  ‘cfv 6232  (class class class)co 7023   ∈ cmpo 7025  1_oc1o 7953  Basecbs 16316  Scalarcsca 16401  X_scprds 16552   “_s cimas 16610   ×_s cxps 16612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-iota 6196  df-fun 6234  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-xps 16616

This theorem is referenced by:  xpsbas  16678  xpsadd  16680  xpsmul  16681  xpssca  16682  xpsvsca  16683  xpsless  16684  xpsle  16685  xpsmnd  17773  xpsgrp  17979  xpstps  22106  xpstopnlem2  22107  xpsdsfn  22674  xpsxmet  22677  xpsdsval  22678  xpsmet  22679  xpsxms  22831  xpsms  22832