Metamath Proof Explorer


Theorem hlhillsm

Description: The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

Ref Expression
Hypotheses hlhil0.h H = LHyp K
hlhil0.l L = DVecH K W
hlhil0.u U = HLHil K W
hlhil0.k φ K HL W H
hlhillsm.a ˙ = LSSum L
Assertion hlhillsm φ ˙ = LSSum U

Proof

Step Hyp Ref Expression
1 hlhil0.h H = LHyp K
2 hlhil0.l L = DVecH K W
3 hlhil0.u U = HLHil K W
4 hlhil0.k φ K HL W H
5 hlhillsm.a ˙ = LSSum L
6 eqidd φ Base L = Base L
7 eqid Base L = Base L
8 1 3 4 2 7 hlhilbase φ Base L = Base U
9 eqid + L = + L
10 1 3 4 2 9 hlhilplus φ + L = + U
11 10 oveqdr φ x Base L y Base L x + L y = x + U y
12 2 fvexi L V
13 12 a1i φ L V
14 3 fvexi U V
15 14 a1i φ U V
16 6 8 11 13 15 lsmpropd φ LSSum L = LSSum U
17 5 16 syl5eq φ ˙ = LSSum U