Metamath Proof Explorer

Theorem latj4rot

Description: Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012)

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

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		simp3l	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B )
5		simp3r	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B )
6	1 2	latjcom	\|- ( ( K e. Lat /\ Z e. B /\ W e. B ) -> ( Z .\/ W ) = ( W .\/ Z ) )
7	3 4 5 6	syl3anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z .\/ W ) = ( W .\/ Z ) )
8	7	oveq2d	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( X .\/ Y ) .\/ ( W .\/ Z ) ) )
9	5 4	jca	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( W e. B /\ Z e. B ) )
10	1 2	latj4	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( W e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ ( W .\/ Z ) ) = ( ( X .\/ W ) .\/ ( Y .\/ Z ) ) )
11	9 10	syld3an3	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( W .\/ Z ) ) = ( ( X .\/ W ) .\/ ( Y .\/ Z ) ) )
12		simp2l	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B )
13	1 2	latjcom	\|- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X .\/ W ) = ( W .\/ X ) )
14	3 12 5 13	syl3anc	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X .\/ W ) = ( W .\/ X ) )
15	14	oveq1d	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ W ) .\/ ( Y .\/ Z ) ) = ( ( W .\/ X ) .\/ ( Y .\/ Z ) ) )
16	8 11 15	3eqtrd	\|- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( W .\/ X ) .\/ ( Y .\/ Z ) ) )