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 ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 unss ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
2 simp1 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ∈ Sℋ )
3 shss ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ )
4 2 3 syl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ⊆ ℋ )
5 simp2 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ∈ Sℋ )
6 shss ⊢ ( 𝐵 ∈ Sℋ → 𝐵 ⊆ ℋ )
7 5 6 syl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ⊆ ℋ )
8 4 7 unssd ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℋ )
9 chss ⊢ ( 𝐶 ∈ Cℋ → 𝐶 ⊆ ℋ )
10 9 3ad2ant3 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐶 ⊆ ℋ )
11 occon2 ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ℋ ∧ 𝐶 ⊆ ℋ ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) ) )
12 8 10 11 syl2anc ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) ) )
13 1 12 syl5bi ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) ) )
14 shjval ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
15 2 5 14 syl2anc ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
16 ococ ⊢ ( 𝐶 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) = 𝐶 )
17 16 3ad2ant3 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) = 𝐶 )
18 17 eqcomd ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐶 = ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) )
19 15 18 sseq12d ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐶 ) ) ) )
20 13 19 sylibrd ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) )
21 shub1 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
22 2 5 21 syl2anc ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
23 sstr ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )
24 22 23 sylan ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )
25 shub2 ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
26 5 2 25 syl2anc ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
27 sstr ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
28 26 27 sylan ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
29 24 28 jca ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) )
30 29 ex ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 → ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ) )
31 20 30 impbid ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 ) )