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

Metamath Proof Explorer

Theorem latj4

Description: Rearrangement of lattice join of 4 classes. ( chj4 analog.) (Contributed by NM, 14-Jun-2012)

		Ref	Expression
	Hypotheses	latjass.b	\|- B = ( Base ` K )
		latjass.j	\|- .\/ = ( join ` K )
	Assertion	latj4	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( X .\/ Z ) .\/ ( Y .\/ W ) ) )

Proof

Step	Hyp	Ref	Expression
1		latjass.b	\|- B = ( Base ` K )
2		latjass.j	\|- .\/ = ( join ` K )
3		simp1	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> K e. Lat )
4		simp2r	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Y e. B )
5		simp3l	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B )
6		simp3r	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B )
7	1 2	latj12	\|- ( ( K e. Lat /\ ( Y e. B /\ Z e. B /\ W e. B ) ) -> ( Y .\/ ( Z .\/ W ) ) = ( Z .\/ ( Y .\/ W ) ) )
8	3 4 5 6 7	syl13anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .\/ ( Z .\/ W ) ) = ( Z .\/ ( Y .\/ W ) ) )
9	8	oveq2d	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .\/ ( Y .\/ ( Z .\/ W ) ) ) = ( X .\/ ( Z .\/ ( Y .\/ W ) ) ) )
10		simp2l	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B )
11	1 2	latjcl	\|- ( ( K e. Lat /\ Z e. B /\ W e. B ) -> ( Z .\/ W ) e. B )
12	3 5 6 11	syl3anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .\/ W ) e. B )
13	1 2	latjass	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ ( Z .\/ W ) e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( X .\/ ( Y .\/ ( Z .\/ W ) ) ) )
14	3 10 4 12 13	syl13anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( X .\/ ( Y .\/ ( Z .\/ W ) ) ) )
15	1 2	latjcl	\|- ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y .\/ W ) e. B )
16	3 4 6 15	syl3anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .\/ W ) e. B )
17	1 2	latjass	\|- ( ( K e. Lat /\ ( X e. B /\ Z e. B /\ ( Y .\/ W ) e. B ) ) -> ( ( X .\/ Z ) .\/ ( Y .\/ W ) ) = ( X .\/ ( Z .\/ ( Y .\/ W ) ) ) )
18	3 10 5 16 17	syl13anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Z ) .\/ ( Y .\/ W ) ) = ( X .\/ ( Z .\/ ( Y .\/ W ) ) ) )
19	9 14 18	3eqtr4d	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( X .\/ Z ) .\/ ( Y .\/ W ) ) )