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

Theorem xpsval 17523
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 3494 . . 3 (πœ‘ β†’ 𝑅 ∈ V)
4 xpsval.2 . . . 4 (πœ‘ β†’ 𝑆 ∈ π‘Š)
54elexd 3494 . . 3 (πœ‘ β†’ 𝑆 ∈ V)
6 fveq2 6891 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
7 xpsval.x . . . . . . . . 9 𝑋 = (Baseβ€˜π‘…)
86, 7eqtr4di 2789 . . . . . . . 8 (π‘Ÿ = 𝑅 β†’ (Baseβ€˜π‘Ÿ) = 𝑋)
9 fveq2 6891 . . . . . . . . 9 (𝑠 = 𝑆 β†’ (Baseβ€˜π‘ ) = (Baseβ€˜π‘†))
10 xpsval.y . . . . . . . . 9 π‘Œ = (Baseβ€˜π‘†)
119, 10eqtr4di 2789 . . . . . . . 8 (𝑠 = 𝑆 β†’ (Baseβ€˜π‘ ) = π‘Œ)
12 mpoeq12 7485 . . . . . . . 8 (((Baseβ€˜π‘Ÿ) = 𝑋 ∧ (Baseβ€˜π‘ ) = π‘Œ) β†’ (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
138, 11, 12syl2an 595 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}))
14 xpsval.f . . . . . . 7 𝐹 = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©})
1513, 14eqtr4di 2789 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ (π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = 𝐹)
1615cnveqd 5875 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ β—‘(π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) = ◑𝐹)
17 fveq2 6891 . . . . . . . . 9 (π‘Ÿ = 𝑅 β†’ (Scalarβ€˜π‘Ÿ) = (Scalarβ€˜π‘…))
1817adantr 480 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ (Scalarβ€˜π‘Ÿ) = (Scalarβ€˜π‘…))
19 xpsval.k . . . . . . . 8 𝐺 = (Scalarβ€˜π‘…)
2018, 19eqtr4di 2789 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ (Scalarβ€˜π‘Ÿ) = 𝐺)
21 simpl 482 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ π‘Ÿ = 𝑅)
2221opeq2d 4880 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ βŸ¨βˆ…, π‘ŸβŸ© = βŸ¨βˆ…, π‘…βŸ©)
23 simpr 484 . . . . . . . . 9 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ 𝑠 = 𝑆)
2423opeq2d 4880 . . . . . . . 8 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ ⟨1o, π‘ βŸ© = ⟨1o, π‘†βŸ©)
2522, 24preq12d 4745 . . . . . . 7 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ {βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©} = {βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})
2620, 25oveq12d 7430 . . . . . 6 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©}) = (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©}))
27 xpsval.u . . . . . 6 π‘ˆ = (𝐺Xs{βŸ¨βˆ…, π‘…βŸ©, ⟨1o, π‘†βŸ©})
2826, 27eqtr4di 2789 . . . . 5 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©}) = π‘ˆ)
2916, 28oveq12d 7430 . . . 4 ((π‘Ÿ = 𝑅 ∧ 𝑠 = 𝑆) β†’ (β—‘(π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©})) = (◑𝐹 β€œs π‘ˆ))
30 df-xps 17463 . . . 4 Γ—s = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ (β—‘(π‘₯ ∈ (Baseβ€˜π‘Ÿ), 𝑦 ∈ (Baseβ€˜π‘ ) ↦ {βŸ¨βˆ…, π‘₯⟩, ⟨1o, π‘¦βŸ©}) β€œs ((Scalarβ€˜π‘Ÿ)Xs{βŸ¨βˆ…, π‘ŸβŸ©, ⟨1o, π‘ βŸ©})))
31 ovex 7445 . . . 4 (◑𝐹 β€œs π‘ˆ) ∈ V
3229, 30, 31ovmpoa 7566 . . 3 ((𝑅 ∈ V ∧ 𝑆 ∈ V) β†’ (𝑅 Γ—s 𝑆) = (◑𝐹 β€œs π‘ˆ))
333, 5, 32syl2anc 583 . 2 (πœ‘ β†’ (𝑅 Γ—s 𝑆) = (◑𝐹 β€œs π‘ˆ))
341, 33eqtrid 2783 1 (πœ‘ β†’ 𝑇 = (◑𝐹 β€œs π‘ˆ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  Vcvv 3473  βˆ…c0 4322  {cpr 4630  βŸ¨cop 4634  β—‘ccnv 5675  β€˜cfv 6543  (class class class)co 7412   ∈ cmpo 7414  1oc1o 8465  Basecbs 17151  Scalarcsca 17207  Xscprds 17398   β€œs cimas 17457   Γ—s cxps 17459
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-xps 17463
This theorem is referenced by:  xpsbas  17525  xpsadd  17527  xpsmul  17528  xpssca  17529  xpsvsca  17530  xpsless  17531  xpsle  17532  xpsmnd  18705  xpsgrp  18985  xpsrngd  20080  xpsringd  20227  xpstps  23634  xpstopnlem2  23635  xpsdsfn  24203  xpsxmet  24206  xpsdsval  24207  xpsmet  24208  xpsxms  24363  xpsms  24364
  Copyright terms: Public domain W3C validator