Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Subspaces and projections
Subspace sum, span, lattice join, lattice supremum
shlej1i
Metamath Proof Explorer
Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM , 19-Oct-1999) (Revised by Mario Carneiro , 15-May-2014)
(New usage is discouraged.)
Ref
Expression
Hypotheses
shincl.1
⊢ 𝐴 ∈ S ℋ
shincl.2
⊢ 𝐵 ∈ S ℋ
shless.1
⊢ 𝐶 ∈ S ℋ
Assertion
shlej1i
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
shincl.1
⊢ 𝐴 ∈ S ℋ
2
shincl.2
⊢ 𝐵 ∈ S ℋ
3
shless.1
⊢ 𝐶 ∈ S ℋ
4
shlej1
⊢ ( ( ( 𝐴 ∈ S ℋ ∧ 𝐵 ∈ S ℋ ∧ 𝐶 ∈ S ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
5
4
ex
⊢ ( ( 𝐴 ∈ S ℋ ∧ 𝐵 ∈ S ℋ ∧ 𝐶 ∈ S ℋ ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) ) )
6
1 2 3 5
mp3an
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )