Theorem latmmdiN

Description: Lattice meet distributes over itself. ( inindi analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	olmass.b	|- B = ( Base ` K )
	olmass.m	|- ./\ = ( meet ` K )
Assertion	latmmdiN	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y ./\ Z ) ) = ( ( X ./\ Y ) ./\ ( X ./\ Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		olmass.b	|- B = ( Base ` K )
2		olmass.m	|- ./\ = ( meet ` K )
3		ollat	|- ( K e. OL -> K e. Lat )
4	3	adantr	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
5		simpr1	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
6	1 2	latmidm	|- ( ( K e. Lat /\ X e. B ) -> ( X ./\ X ) = X )
7	4 5 6	syl2anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ X ) = X )
8	7	oveq1d	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ X ) ./\ ( Y ./\ Z ) ) = ( X ./\ ( Y ./\ Z ) ) )
9		simpl	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OL )
10		simpr2	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
11		simpr3	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
12	1 2	latm4	|- ( ( K e. OL /\ ( X e. B /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) -> ( ( X ./\ X ) ./\ ( Y ./\ Z ) ) = ( ( X ./\ Y ) ./\ ( X ./\ Z ) ) )
13	9 5 5 10 11 12	syl122anc	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ X ) ./\ ( Y ./\ Z ) ) = ( ( X ./\ Y ) ./\ ( X ./\ Z ) ) )
14	8 13	eqtr3d	|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y ./\ Z ) ) = ( ( X ./\ Y ) ./\ ( X ./\ Z ) ) )