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

Theorem pwsval 14865
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 3104 . . 3  |-  ( R  e.  V  ->  R  e.  _V )
3 elex 3104 . . 3  |-  ( I  e.  W  ->  I  e.  _V )
4 simpl 457 . . . . . . 7  |-  ( ( r  =  R  /\  i  =  I )  ->  r  =  R )
54fveq2d 5860 . . . . . 6  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  (Scalar `  R )
)
6 pwsval.f . . . . . 6  |-  F  =  (Scalar `  R )
75, 6syl6eqr 2502 . . . . 5  |-  ( ( r  =  R  /\  i  =  I )  ->  (Scalar `  r )  =  F )
8 id 22 . . . . . 6  |-  ( i  =  I  ->  i  =  I )
9 sneq 4024 . . . . . 6  |-  ( r  =  R  ->  { r }  =  { R } )
10 xpeq12 5008 . . . . . 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 6299 . . . 4  |-  ( ( r  =  R  /\  i  =  I )  ->  ( (Scalar `  r
) X_s ( i  X.  {
r } ) )  =  ( F X_s (
I  X.  { R } ) ) )
13 df-pws 14829 . . . 4  |-  ^s  =  ( r  e.  _V , 
i  e.  _V  |->  ( (Scalar `  r ) X_s ( i  X.  { r } ) ) )
14 ovex 6309 . . . 4  |-  ( F
X_s ( I  X.  { R } ) )  e. 
_V
1512, 13, 14ovmpt2a 6418 . . 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 2496 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 1383    e. wcel 1804   _Vcvv 3095   {csn 4014    X. cxp 4987   ` cfv 5578  (class class class)co 6281  Scalarcsca 14682   X_scprds 14825    ^s cpws 14826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-pws 14829
This theorem is referenced by:  pwsbas  14866  pwsplusgval  14869  pwsmulrval  14870  pwsle  14871  pwsvscafval  14873  pwssca  14875  pwsmnd  15934  pws0g  15935  pwspjmhm  15978  pwsgrp  16160  pwsinvg  16161  pwscmn  16848  pwsabl  16849  pwsgsum  16988  pwsgsumOLD  16989  pwsring  17243  pws1  17244  pwscrng  17245  pwsmgp  17246  pwslmod  17595  frlmpws  18759  frlmlss  18760  frlmpwsfi  18761  frlmbas  18764  frlmbasOLD  18765  frlmip  18787  pwstps  20109  resspwsds  20853  pwsxms  21013  pwsms  21014  rrxprds  21799  cnpwstotbnd  30269  repwsmet  30306  rrnequiv  30307
  Copyright terms: Public domain W3C validator