Metamath Proof Explorer

Theorem shlej1

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion shlej1 ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
2 unss1 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) )
3 simpl1 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ Sℋ )
4 shss ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ )
5 3 4 syl ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ℋ )
6 simpl3 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐶 ∈ Sℋ )
7 shss ⊢ ( 𝐶 ∈ Sℋ → 𝐶 ⊆ ℋ )
8 6 7 syl ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐶 ⊆ ℋ )
9 5 8 unssd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∪ 𝐶 ) ⊆ ℋ )
10 simpl2 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ∈ Sℋ )
11 shss ⊢ ( 𝐵 ∈ Sℋ → 𝐵 ⊆ ℋ )
12 10 11 syl ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐵 ⊆ ℋ )
13 12 8 unssd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∪ 𝐶 ) ⊆ ℋ )
14 occon2 ⊢ ( ( ( 𝐴 ∪ 𝐶 ) ⊆ ℋ ∧ ( 𝐵 ∪ 𝐶 ) ⊆ ℋ ) → ( ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) ) )
15 9 13 14 syl2anc ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) ) )
16 2 15 syl5 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) ) )
17 1 16 mpd ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) )
18 shjval ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐶 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) )
19 3 6 18 syl2anc ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐶 ) ) ) )
20 shjval ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐵 ∨ℋ 𝐶 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) )
21 10 6 20 syl2anc ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∨ℋ 𝐶 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐵 ∪ 𝐶 ) ) ) )
22 17 19 21 3sstr4d ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )