This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme22d

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme22.l 
 |-  .<_ = ( le ` K )
2 cdleme22.j 
 |-  .\/ = ( join ` K )
3 cdleme22.m 
 |-  ./\ = ( meet ` K )
4 cdleme22.a 
 |-  A = ( Atoms ` K )
5 cdleme22.h 
 |-  H = ( LHyp ` K )
6 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> S .<_ ( T .\/ V ) )
7 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> K e. HL )
8 simp22l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> T e. A )
9 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> V e. A )
10 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ T e. A /\ V e. A ) -> T .<_ ( T .\/ V ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> T .<_ ( T .\/ V ) )
12 7 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> K e. Lat )
13 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> S e. A )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 14 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
16 13 15 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> S e. ( Base ` K ) )
17 14 4 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
18 8 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> T e. ( Base ` K ) )
19 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ V e. A ) -> ( T .\/ V ) e. ( Base ` K ) )
20 7 8 9 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( T .\/ V ) e. ( Base ` K ) )
21 14 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ ( T .\/ V ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( T .\/ V ) /\ T .<_ ( T .\/ V ) ) <-> ( S .\/ T ) .<_ ( T .\/ V ) ) )
22 12 16 18 20 21 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .<_ ( T .\/ V ) /\ T .<_ ( T .\/ V ) ) <-> ( S .\/ T ) .<_ ( T .\/ V ) ) )
23 6 11 22 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( S .\/ T ) .<_ ( T .\/ V ) )
24 14 2 4 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
25 7 13 8 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( S .\/ T ) e. ( Base ` K ) )
26 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> W e. H )
27 14 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
28 26 27 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> W e. ( Base ` K ) )
29 14 1 3 latmlem1 
 |-  ( ( K e. Lat /\ ( ( S .\/ T ) e. ( Base ` K ) /\ ( T .\/ V ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( S .\/ T ) .<_ ( T .\/ V ) -> ( ( S .\/ T ) ./\ W ) .<_ ( ( T .\/ V ) ./\ W ) ) )
30 12 25 20 28 29 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .\/ T ) .<_ ( T .\/ V ) -> ( ( S .\/ T ) ./\ W ) .<_ ( ( T .\/ V ) ./\ W ) ) )
31 23 30 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .\/ T ) ./\ W ) .<_ ( ( T .\/ V ) ./\ W ) )
32 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( K e. HL /\ W e. H ) )
33 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( T e. A /\ -. T .<_ W ) )
34 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
35 1 3 34 4 5 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T e. A /\ -. T .<_ W ) ) -> ( T ./\ W ) = ( 0. ` K ) )
36 32 33 35 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( T ./\ W ) = ( 0. ` K ) )
37 36 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( T ./\ W ) .\/ V ) = ( ( 0. ` K ) .\/ V ) )
38 simp23r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> V .<_ W )
39 14 1 2 3 4 atmod4i1 
 |-  ( ( K e. HL /\ ( V e. A /\ T e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ V .<_ W ) -> ( ( T ./\ W ) .\/ V ) = ( ( T .\/ V ) ./\ W ) )
40 7 9 18 28 38 39 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( T ./\ W ) .\/ V ) = ( ( T .\/ V ) ./\ W ) )
41 hlol 
 |-  ( K e. HL -> K e. OL )
42 7 41 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> K e. OL )
43 14 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
44 9 43 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> V e. ( Base ` K ) )
45 14 2 34 olj02 
 |-  ( ( K e. OL /\ V e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ V ) = V )
46 42 44 45 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( 0. ` K ) .\/ V ) = V )
47 37 40 46 3eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( T .\/ V ) ./\ W ) = V )
48 31 47 breqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .\/ T ) ./\ W ) .<_ V )
49 hlatl 
 |-  ( K e. HL -> K e. AtLat )
50 7 49 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> K e. AtLat )
51 simp21r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> -. S .<_ W )
52 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> S =/= T )
53 1 2 3 4 5 lhpat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ S =/= T ) ) -> ( ( S .\/ T ) ./\ W ) e. A )
54 7 26 13 51 8 52 53 syl222anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .\/ T ) ./\ W ) e. A )
55 1 4 atcmp 
 |-  ( ( K e. AtLat /\ ( ( S .\/ T ) ./\ W ) e. A /\ V e. A ) -> ( ( ( S .\/ T ) ./\ W ) .<_ V <-> ( ( S .\/ T ) ./\ W ) = V ) )
56 50 54 9 55 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( ( S .\/ T ) ./\ W ) .<_ V <-> ( ( S .\/ T ) ./\ W ) = V ) )
57 48 56 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> ( ( S .\/ T ) ./\ W ) = V )
58 57 eqcomd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( S =/= T /\ S .<_ ( T .\/ V ) ) ) -> V = ( ( S .\/ T ) ./\ W ) )