Theorem chj4

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

	Ref	Expression
Assertion	chj4	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		chj12	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\to B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)$$
2	1	3expb	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)$$
3	2	adantll	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)$$
4	3	oveq2d	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)\right)=A{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)\right)$$
5		chjcl	$$⊢\left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\to C{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
6		chjass	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)\right)$$
7	6	3expa	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge C{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)\right)$$
8	5 7	sylan2	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)\right)$$
9		chjcl	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\to B{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
10		chjass	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\wedge B{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)\right)$$
11	10	3expa	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)\right)$$
12	9 11	sylan2	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)\right)$$
13	12	an4s	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)=A{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)\right)$$
14	4 8 13	3eqtr4d	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(C\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\right)\to \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}D\right)=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}D\right)$$