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

Theorem pwsval 14990
Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
Hypotheses
Ref Expression
pwsval.y  |-  Y  =  ( R  ^s  I )
pwsval.f  |-  F  =  (Scalar `  R )
Assertion
Ref Expression
pwsval  |-  ( ( R  e.  V  /\  I  e.  W )  ->  Y  =  ( F
X_s ( I  X.  { R } ) ) )

Proof of Theorem pwsval
Dummy variables  i 
r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwsval.y . 2  |-  Y  =  ( R  ^s  I )
2 elex 3065 . . 3  |-  ( R  e.  V  ->  R  e.  _V )
3 elex 3065 . . 3  |-  ( I  e.  W  ->  I  e.  _V )
4 simpl 455 . . . . . . 7  |-  ( ( r  =  R  /\  i  =  I )  ->  r  =  R )
54fveq2d 5807 . . . . . 6  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  (Scalar `  R )
)
6 pwsval.f . . . . . 6  |-  F  =  (Scalar `  R )
75, 6syl6eqr 2459 . . . . 5  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  F )
8 id 22 . . . . . 6  |-  ( i  =  I  ->  i  =  I )
9 sneq 3979 . . . . . 6  |-  ( r  =  R  ->  { r }  =  { R } )
10 xpeq12 4959 . . . . . 6  |-  ( ( i  =  I  /\  { r }  =  { R } )  ->  (
i  X.  { r } )  =  ( I  X.  { R } ) )
118, 9, 10syl2anr 476 . . . . 5  |-  ( ( r  =  R  /\  i  =  I )  ->  ( i  X.  {
r } )  =  ( I  X.  { R } ) )
127, 11oveq12d 6250 . . . 4  |-  ( ( r  =  R  /\  i  =  I )  ->  ( (Scalar `  r
) X_s ( i  X.  {
r } ) )  =  ( F X_s (
I  X.  { R } ) ) )
13 df-pws 14954 . . . 4  |-  ^s  =  ( r  e.  _V , 
i  e.  _V  |->  ( (Scalar `  r ) X_s ( i  X.  { r } ) ) )
14 ovex 6260 . . . 4  |-  ( F
X_s ( I  X.  { R } ) )  e. 
_V
1512, 13, 14ovmpt2a 6368 . . 3  |-  ( ( R  e.  _V  /\  I  e.  _V )  ->  ( R  ^s  I )  =  ( F X_s (
I  X.  { R } ) ) )
162, 3, 15syl2an 475 . 2  |-  ( ( R  e.  V  /\  I  e.  W )  ->  ( R  ^s  I )  =  ( F X_s (
I  X.  { R } ) ) )
171, 16syl5eq 2453 1  |-  ( ( R  e.  V  /\  I  e.  W )  ->  Y  =  ( F
X_s ( I  X.  { R } ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1403    e. wcel 1840   _Vcvv 3056   {csn 3969    X. cxp 4938   ` cfv 5523  (class class class)co 6232  Scalarcsca 14802   X_scprds 14950    ^s cpws 14951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514  ax-nul 4522  ax-pr 4627
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-sbc 3275  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-opab 4451  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-iota 5487  df-fun 5525  df-fv 5531  df-ov 6235  df-oprab 6236  df-mpt2 6237  df-pws 14954
This theorem is referenced by:  pwsbas  14991  pwsplusgval  14994  pwsmulrval  14995  pwsle  14996  pwsvscafval  14998  pwssca  15000  pwsmnd  16169  pws0g  16170  pwspjmhm  16213  pwsgrp  16395  pwsinvg  16396  pwscmn  17083  pwsabl  17084  pwsgsum  17219  pwsgsumOLD  17220  pwsring  17474  pws1  17475  pwscrng  17476  pwsmgp  17477  pwslmod  17826  frlmpws  18969  frlmlss  18970  frlmpwsfi  18971  frlmbas  18974  frlmbasOLD  18975  frlmip  18995  pwstps  20313  resspwsds  21057  pwsxms  21217  pwsms  21218  rrxprds  22003  cnpwstotbnd  31539  repwsmet  31576  rrnequiv  31577
  Copyright terms: Public domain W3C validator