Metamath Proof Explorer


Theorem hlhilsplus2

Description: Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilsbase.h H = LHyp K
hlhilsbase.l L = DVecH K W
hlhilsbase.s S = Scalar L
hlhilsbase.u U = HLHil K W
hlhilsbase.r R = Scalar U
hlhilsbase.k φ K HL W H
hlhilsplus2.a + ˙ = + S
Assertion hlhilsplus2 φ + ˙ = + R

Proof

Step Hyp Ref Expression
1 hlhilsbase.h H = LHyp K
2 hlhilsbase.l L = DVecH K W
3 hlhilsbase.s S = Scalar L
4 hlhilsbase.u U = HLHil K W
5 hlhilsbase.r R = Scalar U
6 hlhilsbase.k φ K HL W H
7 hlhilsplus2.a + ˙ = + S
8 eqid EDRing K W = EDRing K W
9 1 8 2 3 dvhsca K HL W H S = EDRing K W
10 6 9 syl φ S = EDRing K W
11 10 fveq2d φ + S = + EDRing K W
12 7 11 syl5eq φ + ˙ = + EDRing K W
13 eqid + EDRing K W = + EDRing K W
14 1 8 4 5 6 13 hlhilsplus φ + EDRing K W = + R
15 12 14 eqtrd φ + ˙ = + R