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

Theorem pwsval 17529
Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
Hypotheses
Ref Expression
pwsval.y 𝑌 = (𝑅s 𝐼)
pwsval.f 𝐹 = (Scalar‘𝑅)
Assertion
Ref Expression
pwsval ((𝑅𝑉𝐼𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅})))

Proof of Theorem pwsval
Dummy variables 𝑖 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwsval.y . 2 𝑌 = (𝑅s 𝐼)
2 elex 3478 . . 3 (𝑅𝑉𝑅 ∈ V)
3 elex 3478 . . 3 (𝐼𝑊𝐼 ∈ V)
4 simpl 487 . . . . . . 7 ((𝑟 = 𝑅𝑖 = 𝐼) → 𝑟 = 𝑅)
54fveq2d 6875 . . . . . 6 ((𝑟 = 𝑅𝑖 = 𝐼) → (Scalar‘𝑟) = (Scalar‘𝑅))
6 pwsval.f . . . . . 6 𝐹 = (Scalar‘𝑅)
75, 6eqtr4di 2818 . . . . 5 ((𝑟 = 𝑅𝑖 = 𝐼) → (Scalar‘𝑟) = 𝐹)
8 id 23 . . . . . 6 (𝑖 = 𝐼𝑖 = 𝐼)
9 sneq 4595 . . . . . 6 (𝑟 = 𝑅 → {𝑟} = {𝑅})
10 xpeq12 5677 . . . . . 6 ((𝑖 = 𝐼 ∧ {𝑟} = {𝑅}) → (𝑖 × {𝑟}) = (𝐼 × {𝑅}))
118, 9, 10syl2anr 608 . . . . 5 ((𝑟 = 𝑅𝑖 = 𝐼) → (𝑖 × {𝑟}) = (𝐼 × {𝑅}))
127, 11oveq12d 7418 . . . 4 ((𝑟 = 𝑅𝑖 = 𝐼) → ((Scalar‘𝑟)Xs(𝑖 × {𝑟})) = (𝐹Xs(𝐼 × {𝑅})))
13 df-pws 17492 . . . 4 s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
14 ovex 7433 . . . 4 (𝐹Xs(𝐼 × {𝑅})) ∈ V
1512, 13, 14ovmpoa 7555 . . 3 ((𝑅 ∈ V ∧ 𝐼 ∈ V) → (𝑅s 𝐼) = (𝐹Xs(𝐼 × {𝑅})))
162, 3, 15syl2an 607 . 2 ((𝑅𝑉𝐼𝑊) → (𝑅s 𝐼) = (𝐹Xs(𝐼 × {𝑅})))
171, 16eqtrid 2812 1 ((𝑅𝑉𝐼𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 400   = wceq 1563  wcel 2145  Vcvv 3457  {csn 4585   × cxp 5650  cfv 6525  (class class class)co 7400  Scalarcsca 17303  Xscprds 17488  s cpws 17489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-pws 17492
This theorem is referenced by:  pwsbas  17530  pwsplusgval  17534  pwsmulrval  17535  pwsle  17536  pwsvscafval  17538  pwssca  17540  pwsmnd  18820  pws0g  18821  pwspjmhm  18879  pwsgrp  19109  pwsinvg  19110  pwscmn  19924  pwsabl  19925  pwsgsum  20043  pwsring  20396  pws1  20397  pwscrng  20398  pwsmgp  20399  pwslmod  21060  frlmpws  21860  frlmlss  21861  frlmpwsfi  21862  frlmbas  21865  frlmip  21888  pwstps  23748  resspwsds  24490  pwsxms  24650  pwsms  24651  rrxprds  25509  cnpwstotbnd  38308  repwsmet  38345  rrnequiv  38346
  Copyright terms: Public domain W3C validator