Metamath Proof Explorer

Theorem cdleme22aa

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 3rd line on p. 115. Show that t \/ v = p \/ q implies v = u. (Contributed by NM, 2-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 )
cdleme22.u 
|- U = ( ( P .\/ Q ) ./\ W )
Assertion cdleme22aa 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V = U )

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 cdleme22.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
7 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V .<_ ( P .\/ Q ) )
8 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V .<_ W )
9 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> K e. HL )
10 9 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> K e. Lat )
11 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V e. A )
12 eqid 
 |-  ( Base ` K ) = ( Base ` K )
13 12 4 atbase 
 |-  ( V e. A -> V e. ( Base ` K ) )
14 11 13 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V e. ( Base ` K ) )
15 simp21l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> P e. A )
16 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> Q e. A )
17 12 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
18 9 15 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
19 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> W e. H )
20 12 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
21 19 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> W e. ( Base ` K ) )
22 12 1 3 latlem12 
 |-  ( ( K e. Lat /\ ( V e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( V .<_ ( P .\/ Q ) /\ V .<_ W ) <-> V .<_ ( ( P .\/ Q ) ./\ W ) ) )
23 10 14 18 21 22 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> ( ( V .<_ ( P .\/ Q ) /\ V .<_ W ) <-> V .<_ ( ( P .\/ Q ) ./\ W ) ) )
24 7 8 23 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V .<_ ( ( P .\/ Q ) ./\ W ) )
25 24 6 breqtrrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V .<_ U )
26 hlatl 
 |-  ( K e. HL -> K e. AtLat )
27 9 26 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> K e. AtLat )
28 simp21r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> -. P .<_ W )
29 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> P =/= Q )
30 1 2 3 4 5 6 cdleme0a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> U e. A )
31 9 19 15 28 16 29 30 syl222anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> U e. A )
32 1 4 atcmp 
 |-  ( ( K e. AtLat /\ V e. A /\ U e. A ) -> ( V .<_ U <-> V = U ) )
33 27 11 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> ( V .<_ U <-> V = U ) )
34 25 33 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ V .<_ W /\ V .<_ ( P .\/ Q ) ) ) -> V = U )