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 )