# Metamath Proof Explorer

## Theorem shlub

Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shlub ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}{\vee }_{ℋ}{B}\subseteq {C}\right)$

### Proof

Step Hyp Ref Expression
1 unss ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}\cup {B}\subseteq {C}$
2 simp1 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {A}\in {\mathbf{S}}_{ℋ}$
3 shss ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to {A}\subseteq ℋ$
4 2 3 syl ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq ℋ$
5 simp2 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\in {\mathbf{S}}_{ℋ}$
6 shss ${⊢}{B}\in {\mathbf{S}}_{ℋ}\to {B}\subseteq ℋ$
7 5 6 syl ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\subseteq ℋ$
8 4 7 unssd ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cup {B}\subseteq ℋ$
9 chss ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to {C}\subseteq ℋ$
10 9 3ad2ant3 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {C}\subseteq ℋ$
11 occon2 ${⊢}\left({A}\cup {B}\subseteq ℋ\wedge {C}\subseteq ℋ\right)\to \left({A}\cup {B}\subseteq {C}\to \perp \left(\perp \left({A}\cup {B}\right)\right)\subseteq \perp \left(\perp \left({C}\right)\right)\right)$
12 8 10 11 syl2anc ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cup {B}\subseteq {C}\to \perp \left(\perp \left({A}\cup {B}\right)\right)\subseteq \perp \left(\perp \left({C}\right)\right)\right)$
13 1 12 syl5bi ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to \perp \left(\perp \left({A}\cup {B}\right)\right)\subseteq \perp \left(\perp \left({C}\right)\right)\right)$
14 shjval ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to {A}{\vee }_{ℋ}{B}=\perp \left(\perp \left({A}\cup {B}\right)\right)$
15 2 5 14 syl2anc ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}{B}=\perp \left(\perp \left({A}\cup {B}\right)\right)$
16 ococ ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({C}\right)\right)={C}$
17 16 3ad2ant3 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({C}\right)\right)={C}$
18 17 eqcomd ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {C}=\perp \left(\perp \left({C}\right)\right)$
19 15 18 sseq12d ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{\vee }_{ℋ}{B}\subseteq {C}↔\perp \left(\perp \left({A}\cup {B}\right)\right)\subseteq \perp \left(\perp \left({C}\right)\right)\right)$
20 13 19 sylibrd ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\to {A}{\vee }_{ℋ}{B}\subseteq {C}\right)$
21 shub1 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to {A}\subseteq {A}{\vee }_{ℋ}{B}$
22 2 5 21 syl2anc ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {A}{\vee }_{ℋ}{B}$
23 sstr ${⊢}\left({A}\subseteq {A}{\vee }_{ℋ}{B}\wedge {A}{\vee }_{ℋ}{B}\subseteq {C}\right)\to {A}\subseteq {C}$
24 22 23 sylan ${⊢}\left(\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}{\vee }_{ℋ}{B}\subseteq {C}\right)\to {A}\subseteq {C}$
25 shub2 ${⊢}\left({B}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {\mathbf{S}}_{ℋ}\right)\to {B}\subseteq {A}{\vee }_{ℋ}{B}$
26 5 2 25 syl2anc ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\subseteq {A}{\vee }_{ℋ}{B}$
27 sstr ${⊢}\left({B}\subseteq {A}{\vee }_{ℋ}{B}\wedge {A}{\vee }_{ℋ}{B}\subseteq {C}\right)\to {B}\subseteq {C}$
28 26 27 sylan ${⊢}\left(\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}{\vee }_{ℋ}{B}\subseteq {C}\right)\to {B}\subseteq {C}$
29 24 28 jca ${⊢}\left(\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}{\vee }_{ℋ}{B}\subseteq {C}\right)\to \left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)$
30 29 ex ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{\vee }_{ℋ}{B}\subseteq {C}\to \left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)\right)$
31 20 30 impbid ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}{\vee }_{ℋ}{B}\subseteq {C}\right)$