Metamath Proof Explorer


Theorem shslubi

Description: The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shslub.1 AS
shslub.2 BS
shslub.3 CS
Assertion shslubi ACBCA+BC

Proof

Step Hyp Ref Expression
1 shslub.1 AS
2 shslub.2 BS
3 shslub.3 CS
4 1 3 2 shlessi ACA+BC+B
5 3 2 shscomi C+B=B+C
6 4 5 sseqtrdi ACA+BB+C
7 2 3 3 shlessi BCB+CC+C
8 3 shsidmi C+C=C
9 7 8 sseqtrdi BCB+CC
10 6 9 sylan9ss ACBCA+BC
11 1 2 shsub1i AA+B
12 sstr AA+BA+BCAC
13 11 12 mpan A+BCAC
14 2 1 shsub2i BA+B
15 sstr BA+BA+BCBC
16 14 15 mpan A+BCBC
17 13 16 jca A+BCACBC
18 10 17 impbii ACBCA+BC