Metamath Proof Explorer


Theorem pwsmulrval

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

Ref Expression
Hypotheses pwsplusgval.y Y = R 𝑠 I
pwsplusgval.b B = Base Y
pwsplusgval.r φ R V
pwsplusgval.i φ I W
pwsplusgval.f φ F B
pwsplusgval.g φ G B
pwsmulrval.a · ˙ = R
pwsmulrval.p ˙ = Y
Assertion pwsmulrval φ F ˙ G = F · ˙ f G

Proof

Step Hyp Ref Expression
1 pwsplusgval.y Y = R 𝑠 I
2 pwsplusgval.b B = Base Y
3 pwsplusgval.r φ R V
4 pwsplusgval.i φ I W
5 pwsplusgval.f φ F B
6 pwsplusgval.g φ G B
7 pwsmulrval.a · ˙ = R
8 pwsmulrval.p ˙ = Y
9 eqid Scalar R 𝑠 I × R = Scalar R 𝑠 I × R
10 eqid Base Scalar R 𝑠 I × R = Base Scalar R 𝑠 I × R
11 fvexd φ Scalar R V
12 fnconstg R V I × R Fn I
13 3 12 syl φ I × R Fn I
14 eqid Scalar R = Scalar R
15 1 14 pwsval R V I W Y = Scalar R 𝑠 I × R
16 3 4 15 syl2anc φ Y = Scalar R 𝑠 I × R
17 16 fveq2d φ Base Y = Base Scalar R 𝑠 I × R
18 2 17 eqtrid φ B = Base Scalar R 𝑠 I × R
19 5 18 eleqtrd φ F Base Scalar R 𝑠 I × R
20 6 18 eleqtrd φ G Base Scalar R 𝑠 I × R
21 eqid Scalar R 𝑠 I × R = Scalar R 𝑠 I × R
22 9 10 11 4 13 19 20 21 prdsmulrval φ F Scalar R 𝑠 I × R G = x I F x I × R x G x
23 fvconst2g R V x I I × R x = R
24 3 23 sylan φ x I I × R x = R
25 24 fveq2d φ x I I × R x = R
26 25 7 eqtr4di φ x I I × R x = · ˙
27 26 oveqd φ x I F x I × R x G x = F x · ˙ G x
28 27 mpteq2dva φ x I F x I × R x G x = x I F x · ˙ G x
29 22 28 eqtrd φ F Scalar R 𝑠 I × R G = x I F x · ˙ G x
30 16 fveq2d φ Y = Scalar R 𝑠 I × R
31 8 30 eqtrid φ ˙ = Scalar R 𝑠 I × R
32 31 oveqd φ F ˙ G = F Scalar R 𝑠 I × R G
33 fvexd φ x I F x V
34 fvexd φ x I G x V
35 eqid Base R = Base R
36 1 35 2 3 4 5 pwselbas φ F : I Base R
37 36 feqmptd φ F = x I F x
38 1 35 2 3 4 6 pwselbas φ G : I Base R
39 38 feqmptd φ G = x I G x
40 4 33 34 37 39 offval2 φ F · ˙ f G = x I F x · ˙ G x
41 29 32 40 3eqtr4d φ F ˙ G = F · ˙ f G