Metamath Proof Explorer


Theorem hlhilplus

Description: The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015)

Ref Expression
Hypotheses hlhilbase.h H = LHyp K
hlhilbase.u U = HLHil K W
hlhilbase.k φ K HL W H
hlhilbase.l L = DVecH K W
hlhilplus.a + ˙ = + L
Assertion hlhilplus φ + ˙ = + U

Proof

Step Hyp Ref Expression
1 hlhilbase.h H = LHyp K
2 hlhilbase.u U = HLHil K W
3 hlhilbase.k φ K HL W H
4 hlhilbase.l L = DVecH K W
5 hlhilplus.a + ˙ = + L
6 5 fvexi + ˙ V
7 eqid Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x = Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x
8 7 phlplusg + ˙ V + ˙ = + Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x
9 6 8 ax-mp + ˙ = + Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x
10 eqid Base L = Base L
11 eqid EDRing K W = EDRing K W
12 eqid HGMap K W = HGMap K W
13 eqid EDRing K W sSet * ndx HGMap K W = EDRing K W sSet * ndx HGMap K W
14 eqid L = L
15 eqid HDMap K W = HDMap K W
16 eqid x Base L , y Base L HDMap K W y x = x Base L , y Base L HDMap K W y x
17 1 2 4 10 5 11 12 13 14 15 16 3 hlhilset φ U = Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x
18 17 fveq2d φ + U = + Base ndx Base L + ndx + ˙ Scalar ndx EDRing K W sSet * ndx HGMap K W ndx L 𝑖 ndx x Base L , y Base L HDMap K W y x
19 9 18 eqtr4id φ + ˙ = + U