Theorem latjjdi

Description: Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012)

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

Proof

Step	Hyp	Ref	Expression
1		latjass.b	|- B = ( Base ` K )
2		latjass.j	|- .\/ = ( join ` K )
3		simpr1	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
4	1 2	latjidm	|- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) = X )
5	3 4	syldan	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ X ) = X )
6	5	oveq1d	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ X ) .\/ ( Y .\/ Z ) ) = ( X .\/ ( Y .\/ Z ) ) )
7		simpl	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
8		simpr2	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
9		simpr3	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
10	1 2	latj4	|- ( ( K e. Lat /\ ( X e. B /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) -> ( ( X .\/ X ) .\/ ( Y .\/ Z ) ) = ( ( X .\/ Y ) .\/ ( X .\/ Z ) ) )
11	7 3 3 8 9 10	syl122anc	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ X ) .\/ ( Y .\/ Z ) ) = ( ( X .\/ Y ) .\/ ( X .\/ Z ) ) )
12	6 11	eqtr3d	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( ( X .\/ Y ) .\/ ( X .\/ Z ) ) )