This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shlej2

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

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

Proof

Step Hyp Ref Expression
1 shlej1 ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
2 shjcom ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐴 ) )
3 2 3adant2 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐴 ) )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐴 ) )
5 shjcom ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 ) )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 ) )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 ) )
8 1 4 7 3sstr3d ⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐶 ∨ℋ 𝐵 ) )