Metamath Proof Explorer

Theorem cdleme10

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. D represents s_2. In their notation, we prove s \/ s_2 = s \/ r. (Contributed by NM, 9-Jun-2012)

Ref Expression
Hypotheses cdleme10.l 
|- .<_ = ( le ` K )
cdleme10.j 
|- .\/ = ( join ` K )
cdleme10.m 
|- ./\ = ( meet ` K )
cdleme10.a 
|- A = ( Atoms ` K )
cdleme10.h 
|- H = ( LHyp ` K )
cdleme10.d 
|- D = ( ( R .\/ S ) ./\ W )
Assertion cdleme10 
|- ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ D ) = ( S .\/ R ) )

Proof

Step Hyp Ref Expression
1 cdleme10.l 
 |-  .<_ = ( le ` K )
2 cdleme10.j 
 |-  .\/ = ( join ` K )
3 cdleme10.m 
 |-  ./\ = ( meet ` K )
4 cdleme10.a 
 |-  A = ( Atoms ` K )
5 cdleme10.h 
 |-  H = ( LHyp ` K )
6 cdleme10.d 
 |-  D = ( ( R .\/ S ) ./\ W )
7 6 oveq2i 
 |-  ( S .\/ D ) = ( S .\/ ( ( R .\/ S ) ./\ W ) )
8 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> K e. HL )
9 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> S e. A )
10 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> R e. A )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 2 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
13 8 10 9 12 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ S ) e. ( Base ` K ) )
14 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> W e. H )
15 11 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> W e. ( Base ` K ) )
17 8 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> K e. Lat )
18 11 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
19 18 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> R e. ( Base ` K ) )
20 11 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
21 9 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> S e. ( Base ` K ) )
22 11 1 2 latlej2 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> S .<_ ( R .\/ S ) )
23 17 19 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> S .<_ ( R .\/ S ) )
24 11 1 2 3 4 atmod3i1 
 |-  ( ( K e. HL /\ ( S e. A /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ S .<_ ( R .\/ S ) ) -> ( S .\/ ( ( R .\/ S ) ./\ W ) ) = ( ( R .\/ S ) ./\ ( S .\/ W ) ) )
25 8 9 13 16 23 24 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ ( ( R .\/ S ) ./\ W ) ) = ( ( R .\/ S ) ./\ ( S .\/ W ) ) )
26 11 2 latjcom 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( R .\/ S ) = ( S .\/ R ) )
27 17 19 21 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( R .\/ S ) = ( S .\/ R ) )
28 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
29 1 2 28 4 5 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ W ) = ( 1. ` K ) )
30 29 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ W ) = ( 1. ` K ) )
31 27 30 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( ( R .\/ S ) ./\ ( S .\/ W ) ) = ( ( S .\/ R ) ./\ ( 1. ` K ) ) )
32 hlol 
 |-  ( K e. HL -> K e. OL )
33 8 32 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> K e. OL )
34 11 2 latjcl 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( S .\/ R ) e. ( Base ` K ) )
35 17 21 19 34 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ R ) e. ( Base ` K ) )
36 11 3 28 olm11 
 |-  ( ( K e. OL /\ ( S .\/ R ) e. ( Base ` K ) ) -> ( ( S .\/ R ) ./\ ( 1. ` K ) ) = ( S .\/ R ) )
37 33 35 36 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( ( S .\/ R ) ./\ ( 1. ` K ) ) = ( S .\/ R ) )
38 25 31 37 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ ( ( R .\/ S ) ./\ W ) ) = ( S .\/ R ) )
39 7 38 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ R e. A /\ ( S e. A /\ -. S .<_ W ) ) -> ( S .\/ D ) = ( S .\/ R ) )