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

Theorem xpsval 16434
Description: Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.)
Hypotheses
Ref Expression
xpsval.t 𝑇 = (𝑅 ×s 𝑆)
xpsval.x 𝑋 = (Base‘𝑅)
xpsval.y 𝑌 = (Base‘𝑆)
xpsval.1 (𝜑𝑅𝑉)
xpsval.2 (𝜑𝑆𝑊)
xpsval.f 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
xpsval.k 𝐺 = (Scalar‘𝑅)
xpsval.u 𝑈 = (𝐺Xs({𝑅} +𝑐 {𝑆}))
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 (𝜑𝑅𝑉)
3 elex 3352 . . . 4 (𝑅𝑉𝑅 ∈ V)
42, 3syl 17 . . 3 (𝜑𝑅 ∈ V)
5 xpsval.2 . . . 4 (𝜑𝑆𝑊)
6 elex 3352 . . . 4 (𝑆𝑊𝑆 ∈ V)
75, 6syl 17 . . 3 (𝜑𝑆 ∈ V)
8 fveq2 6352 . . . . . . . . 9 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
9 xpsval.x . . . . . . . . 9 𝑋 = (Base‘𝑅)
108, 9syl6eqr 2812 . . . . . . . 8 (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋)
11 fveq2 6352 . . . . . . . . 9 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
12 xpsval.y . . . . . . . . 9 𝑌 = (Base‘𝑆)
1311, 12syl6eqr 2812 . . . . . . . 8 (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌)
14 mpt2eq12 6880 . . . . . . . 8 (((Base‘𝑟) = 𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
1510, 13, 14syl2an 495 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
16 xpsval.f . . . . . . 7 𝐹 = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
1715, 16syl6eqr 2812 . . . . . 6 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) = 𝐹)
1817cnveqd 5453 . . . . 5 ((𝑟 = 𝑅𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) = 𝐹)
19 fveq2 6352 . . . . . . . . 9 (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅))
2019adantr 472 . . . . . . . 8 ((𝑟 = 𝑅𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅))
21 xpsval.k . . . . . . . 8 𝐺 = (Scalar‘𝑅)
2220, 21syl6eqr 2812 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺)
23 sneq 4331 . . . . . . . . 9 (𝑟 = 𝑅 → {𝑟} = {𝑅})
24 sneq 4331 . . . . . . . . 9 (𝑠 = 𝑆 → {𝑠} = {𝑆})
2523, 24oveqan12d 6832 . . . . . . . 8 ((𝑟 = 𝑅𝑠 = 𝑆) → ({𝑟} +𝑐 {𝑠}) = ({𝑅} +𝑐 {𝑆}))
2625cnveqd 5453 . . . . . . 7 ((𝑟 = 𝑅𝑠 = 𝑆) → ({𝑟} +𝑐 {𝑠}) = ({𝑅} +𝑐 {𝑆}))
2722, 26oveq12d 6831 . . . . . 6 ((𝑟 = 𝑅𝑠 = 𝑆) → ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠})) = (𝐺Xs({𝑅} +𝑐 {𝑆})))
28 xpsval.u . . . . . 6 𝑈 = (𝐺Xs({𝑅} +𝑐 {𝑆}))
2927, 28syl6eqr 2812 . . . . 5 ((𝑟 = 𝑅𝑠 = 𝑆) → ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠})) = 𝑈)
3018, 29oveq12d 6831 . . . 4 ((𝑟 = 𝑅𝑠 = 𝑆) → ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))) = (𝐹s 𝑈))
31 df-xps 16372 . . . 4 ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))))
32 ovex 6841 . . . 4 (𝐹s 𝑈) ∈ V
3330, 31, 32ovmpt2a 6956 . . 3 ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s 𝑆) = (𝐹s 𝑈))
344, 7, 33syl2anc 696 . 2 (𝜑 → (𝑅 ×s 𝑆) = (𝐹s 𝑈))
351, 34syl5eq 2806 1 (𝜑𝑇 = (𝐹s 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  Vcvv 3340  {csn 4321  ccnv 5265  cfv 6049  (class class class)co 6813  cmpt2 6815   +𝑐 ccda 9181  Basecbs 16059  Scalarcsca 16146  Xscprds 16308  s cimas 16366   ×s cxps 16368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-xps 16372
This theorem is referenced by:  xpsbas  16436  xpsadd  16438  xpsmul  16439  xpssca  16440  xpsvsca  16441  xpsless  16442  xpsle  16443  xpsmnd  17531  xpsgrp  17735  xpstps  21815  xpstopnlem2  21816  xpsdsfn  22383  xpsxmet  22386  xpsdsval  22387  xpsmet  22388  xpsxms  22540  xpsms  22541
  Copyright terms: Public domain W3C validator