Metamath Proof Explorer


Theorem pwsval

Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsval.y Y = R 𝑠 I
pwsval.f F = Scalar R
Assertion pwsval R V I W Y = F 𝑠 I × R

Proof

Step Hyp Ref Expression
1 pwsval.y Y = R 𝑠 I
2 pwsval.f F = Scalar R
3 elex R V R V
4 elex I W I V
5 simpl r = R i = I r = R
6 5 fveq2d r = R i = I Scalar r = Scalar R
7 6 2 syl6eqr r = R i = I Scalar r = F
8 id i = I i = I
9 sneq r = R r = R
10 xpeq12 i = I r = R i × r = I × R
11 8 9 10 syl2anr r = R i = I i × r = I × R
12 7 11 oveq12d r = R i = I Scalar r 𝑠 i × r = F 𝑠 I × R
13 df-pws 𝑠 = r V , i V Scalar r 𝑠 i × r
14 ovex F 𝑠 I × R V
15 12 13 14 ovmpoa R V I V R 𝑠 I = F 𝑠 I × R
16 3 4 15 syl2an R V I W R 𝑠 I = F 𝑠 I × R
17 1 16 syl5eq R V I W Y = F 𝑠 I × R