Metamath Proof Explorer

Theorem shjshsi

Description: Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shjshs.1 ⊢ 𝐴 ∈ Sℋ
shjshs.2 ⊢ 𝐵 ∈ Sℋ
Assertion shjshsi ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 shjshs.1 ⊢ 𝐴 ∈ Sℋ
2 shjshs.2 ⊢ 𝐵 ∈ Sℋ
3 shjval ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
4 1 2 3 mp2an ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
5 1 2 shunssi ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )
6 1 shssii ⊢ 𝐴 ⊆ ℋ
7 2 shssii ⊢ 𝐵 ⊆ ℋ
8 6 7 unssi ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ℋ
9 1 2 shscli ⊢ ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ
10 9 shssii ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ
11 8 10 occon2i ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ) )
12 5 11 ax-mp ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )
13 4 12 eqsstri ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )
14 1 2 shsleji ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
15 1 2 shjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
16 15 chssii ⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ℋ
17 occon ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ℋ ) → ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ) )
18 10 16 17 mp2an ⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )
19 14 18 ax-mp ⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) )
20 occl ⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ → ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ∈ Cℋ )
21 10 20 ax-mp ⊢ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ∈ Cℋ
22 15 21 chsscon1i ⊢ ( ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
23 19 22 mpbi ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
24 13 23 eqssi ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )