Theorem dihmeetlem5

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014)

	Ref	Expression
Hypotheses	dihmeetlem5.b	|- B = ( Base ` K )
	dihmeetlem5.l	|- .<_ = ( le ` K )
	dihmeetlem5.j	|- .\/ = ( join ` K )
	dihmeetlem5.m	|- ./\ = ( meet ` K )
	dihmeetlem5.a	|- A = ( Atoms ` K )
Assertion	dihmeetlem5	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( X ./\ ( Y .\/ Q ) ) = ( ( X ./\ Y ) .\/ Q ) )

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem5.b	|- B = ( Base ` K )
2		dihmeetlem5.l	|- .<_ = ( le ` K )
3		dihmeetlem5.j	|- .\/ = ( join ` K )
4		dihmeetlem5.m	|- ./\ = ( meet ` K )
5		dihmeetlem5.a	|- A = ( Atoms ` K )
6		simpl1	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> K e. HL )
7		simprl	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Q e. A )
8		simpl2	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> X e. B )
9		simpl3	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Y e. B )
10		simprr	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Q .<_ X )
11	1 2 3 4 5	atmod2i1	|- ( ( K e. HL /\ ( Q e. A /\ X e. B /\ Y e. B ) /\ Q .<_ X ) -> ( ( X ./\ Y ) .\/ Q ) = ( X ./\ ( Y .\/ Q ) ) )
12	6 7 8 9 10 11	syl131anc	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( ( X ./\ Y ) .\/ Q ) = ( X ./\ ( Y .\/ Q ) ) )
13	12	eqcomd	|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( X ./\ ( Y .\/ Q ) ) = ( ( X ./\ Y ) .\/ Q ) )