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

Metamath Proof Explorer

Theorem chj4i

Description: Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chj12.1 ⊢ 𝐴 ∈ Cℋ
chj12.2 ⊢ 𝐵 ∈ Cℋ
chj12.3 ⊢ 𝐶 ∈ Cℋ
chj4.4 ⊢ 𝐷 ∈ Cℋ
Assertion chj4i ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 chj12.1 ⊢ 𝐴 ∈ Cℋ
2 chj12.2 ⊢ 𝐵 ∈ Cℋ
3 chj12.3 ⊢ 𝐶 ∈ Cℋ
4 chj4.4 ⊢ 𝐷 ∈ Cℋ
5 2 3 4 chj12i ⊢ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )
6 5 oveq2i ⊢ ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) )
7 3 4 chjcli ⊢ ( 𝐶 ∨ℋ 𝐷 ) ∈ Cℋ
8 1 2 7 chjassi ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) )
9 2 4 chjcli ⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Cℋ
10 1 3 9 chjassi ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) ) )
11 6 8 10 3eqtr4i ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ ( 𝐶 ∨ℋ 𝐷 ) ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ ( 𝐵 ∨ℋ 𝐷 ) )