Theorem cdleme42d

Description: Part of proof of Lemma E in Crawley p. 113. Match ( s .\/ ( x ./\ W ) ) = x . (Contributed by NM, 6-Mar-2013)

	Ref	Expression
Hypotheses	cdleme42.b	|- B = ( Base ` K )
	cdleme42.l	|- .<_ = ( le ` K )
	cdleme42.j	|- .\/ = ( join ` K )
	cdleme42.m	|- ./\ = ( meet ` K )
	cdleme42.a	|- A = ( Atoms ` K )
	cdleme42.h	|- H = ( LHyp ` K )
	cdleme42.v	|- V = ( ( R .\/ S ) ./\ W )
Assertion	cdleme42d	|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ ( ( R .\/ V ) ./\ W ) ) = ( R .\/ V ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme42.b	|- B = ( Base ` K )
2		cdleme42.l	|- .<_ = ( le ` K )
3		cdleme42.j	|- .\/ = ( join ` K )
4		cdleme42.m	|- ./\ = ( meet ` K )
5		cdleme42.a	|- A = ( Atoms ` K )
6		cdleme42.h	|- H = ( LHyp ` K )
7		cdleme42.v	|- V = ( ( R .\/ S ) ./\ W )
8	7	oveq2i	|- ( R .\/ V ) = ( R .\/ ( ( R .\/ S ) ./\ W ) )
9	1 2 3 4 5 6 7	cdleme42a	|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ S ) = ( R .\/ V ) )
10	9	oveq1d	|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( ( R .\/ S ) ./\ W ) = ( ( R .\/ V ) ./\ W ) )
11	10	oveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ ( ( R .\/ S ) ./\ W ) ) = ( R .\/ ( ( R .\/ V ) ./\ W ) ) )
12	8 11	eqtr2id	|- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ ( ( R .\/ V ) ./\ W ) ) = ( R .\/ V ) )