Theorem latm4

Description: Rearrangement of lattice meet of 4 classes. ( in4 analog.) (Contributed by NM, 8-Nov-2011)

	Ref	Expression
Hypotheses	olmass.b	|- B = ( Base ` K )
	olmass.m	|- ./\ = ( meet ` K )
Assertion	latm4	|- ( ( K e. OL /\ ( 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		olmass.b	|- B = ( Base ` K )
2		olmass.m	|- ./\ = ( meet ` K )
3		simp1	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> K e. OL )
4		simp2r	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Y e. B )
5		simp3l	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B )
6		simp3r	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B )
7	1 2	latm12	|- ( ( K e. OL /\ ( Y e. B /\ Z e. B /\ W e. B ) ) -> ( Y ./\ ( Z ./\ W ) ) = ( Z ./\ ( Y ./\ W ) ) )
8	3 4 5 6 7	syl13anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y ./\ ( Z ./\ W ) ) = ( Z ./\ ( Y ./\ W ) ) )
9	8	oveq2d	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( X ./\ ( Y ./\ ( Z ./\ W ) ) ) = ( X ./\ ( Z ./\ ( Y ./\ W ) ) ) )
10		simp2l	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B )
11		ollat	|- ( K e. OL -> K e. Lat )
12	11	3ad2ant1	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> K e. Lat )
13	1 2	latmcl	|- ( ( K e. Lat /\ Z e. B /\ W e. B ) -> ( Z ./\ W ) e. B )
14	12 5 6 13	syl3anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Z ./\ W ) e. B )
15	1 2	latmassOLD	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ ( Z ./\ W ) e. B ) ) -> ( ( X ./\ Y ) ./\ ( Z ./\ W ) ) = ( X ./\ ( Y ./\ ( Z ./\ W ) ) ) )
16	3 10 4 14 15	syl13anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X ./\ Y ) ./\ ( Z ./\ W ) ) = ( X ./\ ( Y ./\ ( Z ./\ W ) ) ) )
17	1 2	latmcl	|- ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) e. B )
18	12 4 6 17	syl3anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y ./\ W ) e. B )
19	1 2	latmassOLD	|- ( ( K e. OL /\ ( X e. B /\ Z e. B /\ ( Y ./\ W ) e. B ) ) -> ( ( X ./\ Z ) ./\ ( Y ./\ W ) ) = ( X ./\ ( Z ./\ ( Y ./\ W ) ) ) )
20	3 10 5 18 19	syl13anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X ./\ Z ) ./\ ( Y ./\ W ) ) = ( X ./\ ( Z ./\ ( Y ./\ W ) ) ) )
21	9 16 20	3eqtr4d	|- ( ( K e. OL /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X ./\ Y ) ./\ ( Z ./\ W ) ) = ( ( X ./\ Z ) ./\ ( Y ./\ W ) ) )