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

Theorem pwsval 14427
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 2984 . . 3  |-  ( R  e.  V  ->  R  e.  _V )
3 elex 2984 . . 3  |-  ( I  e.  W  ->  I  e.  _V )
4 simpl 457 . . . . . . 7  |-  ( ( r  =  R  /\  i  =  I )  ->  r  =  R )
54fveq2d 5698 . . . . . 6  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  (Scalar `  R )
)
6 pwsval.f . . . . . 6  |-  F  =  (Scalar `  R )
75, 6syl6eqr 2493 . . . . 5  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  F )
8 id 22 . . . . . 6  |-  ( i  =  I  ->  i  =  I )
9 sneq 3890 . . . . . 6  |-  ( r  =  R  ->  { r }  =  { R } )
10 xpeq12 4862 . . . . . 6  |-  ( ( i  =  I  /\  { r }  =  { R } )  ->  (
i  X.  { r } )  =  ( I  X.  { R } ) )
118, 9, 10syl2anr 478 . . . . 5  |-  ( ( r  =  R  /\  i  =  I )  ->  ( i  X.  {
r } )  =  ( I  X.  { R } ) )
127, 11oveq12d 6112 . . . 4  |-  ( ( r  =  R  /\  i  =  I )  ->  ( (Scalar `  r
) X_s ( i  X.  {
r } ) )  =  ( F X_s (
I  X.  { R } ) ) )
13 df-pws 14391 . . . 4  |-  ^s  =  ( r  e.  _V , 
i  e.  _V  |->  ( (Scalar `  r ) X_s ( i  X.  { r } ) ) )
14 ovex 6119 . . . 4  |-  ( F
X_s ( I  X.  { R } ) )  e. 
_V
1512, 13, 14ovmpt2a 6224 . . 3  |-  ( ( R  e.  _V  /\  I  e.  _V )  ->  ( R  ^s  I )  =  ( F X_s (
I  X.  { R } ) ) )
162, 3, 15syl2an 477 . 2  |-  ( ( R  e.  V  /\  I  e.  W )  ->  ( R  ^s  I )  =  ( F X_s (
I  X.  { R } ) ) )
171, 16syl5eq 2487 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 369    = wceq 1369    e. wcel 1756   _Vcvv 2975   {csn 3880    X. cxp 4841   ` cfv 5421  (class class class)co 6094  Scalarcsca 14244   X_scprds 14387    ^s cpws 14388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-iota 5384  df-fun 5423  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-pws 14391
This theorem is referenced by:  pwsbas  14428  pwsplusgval  14431  pwsmulrval  14432  pwsle  14433  pwsvscafval  14435  pwssca  14437  pwsmnd  15459  pws0g  15460  pwspjmhm  15499  pwsgrp  15669  pwsinvg  15670  pwscmn  16348  pwsabl  16349  pwsgsum  16476  pwsgsumOLD  16477  pwsrng  16710  pws1  16711  pwscrng  16712  pwsmgp  16713  pwslmod  17054  frlmpws  18178  frlmlss  18179  frlmpwsfi  18180  frlmbas  18183  frlmbasOLD  18184  frlmip  18206  pwstps  19206  resspwsds  19950  pwsxms  20110  pwsms  20111  rrxprds  20896  cnpwstotbnd  28699  repwsmet  28736  rrnequiv  28737
  Copyright terms: Public domain W3C validator