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

Metamath Proof Explorer

Theorem shjcom

Description: Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shjcom ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ∨ ℋ B = B ∨ ℋ A

Proof

Step Hyp Ref Expression
1 shjval ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ∨ ℋ B = ⊥ ⁡ ⊥ ⁡ A ∪ B
2 shjval ⊢ B ∈ S ℋ ∧ A ∈ S ℋ → B ∨ ℋ A = ⊥ ⁡ ⊥ ⁡ B ∪ A
3 2 ancoms ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → B ∨ ℋ A = ⊥ ⁡ ⊥ ⁡ B ∪ A
4 uncom ⊢ B ∪ A = A ∪ B
5 4 fveq2i ⊢ ⊥ ⁡ B ∪ A = ⊥ ⁡ A ∪ B
6 5 fveq2i ⊢ ⊥ ⁡ ⊥ ⁡ B ∪ A = ⊥ ⁡ ⊥ ⁡ A ∪ B
7 3 6 eqtrdi ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → B ∨ ℋ A = ⊥ ⁡ ⊥ ⁡ A ∪ B
8 1 7 eqtr4d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ∨ ℋ B = B ∨ ℋ A