Metamath Proof Explorer


Theorem hhssva

Description: The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhss.1 W = + H × H × H norm H
Assertion hhssva + H × H = + v W

Proof

Step Hyp Ref Expression
1 hhss.1 W = + H × H × H norm H
2 eqid + v W = + v W
3 2 vafval + v W = 1 st 1 st W
4 1 fveq2i 1 st W = 1 st + H × H × H norm H
5 opex + H × H × H V
6 normf norm :
7 ax-hilex V
8 fex norm : V norm V
9 6 7 8 mp2an norm V
10 9 resex norm H V
11 5 10 op1st 1 st + H × H × H norm H = + H × H × H
12 4 11 eqtri 1 st W = + H × H × H
13 12 fveq2i 1 st 1 st W = 1 st + H × H × H
14 hilablo + AbelOp
15 resexg + AbelOp + H × H V
16 14 15 ax-mp + H × H V
17 hvmulex V
18 17 resex × H V
19 16 18 op1st 1 st + H × H × H = + H × H
20 3 13 19 3eqtrri + H × H = + v W