Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpsval Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 xpsval.t . 2 𝑇 = (𝑅 ×s 𝑆)
2 xpsval.1 . . . 4 (𝜑𝑅𝑉)
32elexd 3431 . . 3 (𝜑𝑅 ∈ V)
4 xpsval.2 . . . 4 (𝜑𝑆𝑊)
54elexd 3431 . . 3 (𝜑𝑆 ∈ V)
6 fveq2 6659 . . . . . . . . 9 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
7 xpsval.x . . . . . . . . 9 𝑋 = (Base‘𝑅)
86, 7eqtr4di 2812 . . . . . . . 8 (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋)
9 fveq2 6659 . . . . . . . . 9 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
10 xpsval.y . . . . . . . . 9 𝑌 = (Base‘𝑆)
119, 10eqtr4di 2812 . . . . . . . 8 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌)
12 mpoeq12 7222 . . . . . . . 8 (((Base‘𝑟) = 𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
138, 11, 12syl2an 599 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
14 xpsval.f . . . . . . 7 𝐹 = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
1513, 14eqtr4di 2812 . . . . . 6 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = 𝐹)
1615cnveqd 5716 . . . . 5 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = 𝐹)
17 fveq2 6659 . . . . . . . . 9 (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅))
1817adantr 485 . . . . . . . 8 ((𝑟 = 𝑅𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅))
19 xpsval.k . . . . . . . 8 𝐺 = (Scalar‘𝑅)
2018, 19eqtr4di 2812 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺)
21 simpl 487 . . . . . . . . 9 ((𝑟 = 𝑅𝑠 = 𝑆) → 𝑟 = 𝑅)
2221opeq2d 4771 . . . . . . . 8 ((𝑟 = 𝑅𝑠 = 𝑆) → ⟨∅, 𝑟⟩ = ⟨∅, 𝑅⟩)
23 simpr 489 . . . . . . . . 9 ((𝑟 = 𝑅𝑠 = 𝑆) → 𝑠 = 𝑆)
2423opeq2d 4771 . . . . . . . 8 ((𝑟 = 𝑅𝑠 = 𝑆) → ⟨1o, 𝑠⟩ = ⟨1o, 𝑆⟩)
2522, 24preq12d 4635 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩} = {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
2620, 25oveq12d 7169 . . . . . 6 ((𝑟 = 𝑅𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
27 xpsval.u . . . . . 6 𝑈 = (𝐺Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
2826, 27eqtr4di 2812 . . . . 5 ((𝑟 = 𝑅𝑠 = 𝑆) → ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}) = 𝑈)
2916, 28oveq12d 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
3229, 30, 31ovmpoa 7301 . . 3 ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s 𝑆) = (𝐹s 𝑈))
333, 5, 32syl2anc 588 . 2 (𝜑 → (𝑅 ×s 𝑆) = (𝐹s 𝑈))
341, 33syl5eq 2806 1 (𝜑𝑇 = (𝐹s 𝑈))
 Colors of variables: wff setvar class 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  1oc1o 8106  Basecbs 16534  Scalarcsca 16619  Xscprds 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
 Copyright terms: Public domain W3C validator