Metamath Proof Explorer


Theorem cdleme27N

Description: Part of proof of Lemma E in Crawley p. 113. Eliminate the s =/= t antecedent in cdleme27a . (Contributed by NM, 3-Feb-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme26.b B=BaseK
cdleme26.l ˙=K
cdleme26.j ˙=joinK
cdleme26.m ˙=meetK
cdleme26.a A=AtomsK
cdleme26.h H=LHypK
cdleme27.u U=P˙Q˙W
cdleme27.f F=s˙U˙Q˙P˙s˙W
cdleme27.z Z=z˙U˙Q˙P˙z˙W
cdleme27.n N=P˙Q˙Z˙s˙z˙W
cdleme27.d D=ιuB|zA¬z˙W¬z˙P˙Qu=N
cdleme27.c C=ifs˙P˙QDF
cdleme27.g G=t˙U˙Q˙P˙t˙W
cdleme27.o O=P˙Q˙Z˙t˙z˙W
cdleme27.e E=ιuB|zA¬z˙W¬z˙P˙Qu=O
cdleme27.y Y=ift˙P˙QEG
Assertion cdleme27N KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WC˙Y˙V

Proof

Step Hyp Ref Expression
1 cdleme26.b B=BaseK
2 cdleme26.l ˙=K
3 cdleme26.j ˙=joinK
4 cdleme26.m ˙=meetK
5 cdleme26.a A=AtomsK
6 cdleme26.h H=LHypK
7 cdleme27.u U=P˙Q˙W
8 cdleme27.f F=s˙U˙Q˙P˙s˙W
9 cdleme27.z Z=z˙U˙Q˙P˙z˙W
10 cdleme27.n N=P˙Q˙Z˙s˙z˙W
11 cdleme27.d D=ιuB|zA¬z˙W¬z˙P˙Qu=N
12 cdleme27.c C=ifs˙P˙QDF
13 cdleme27.g G=t˙U˙Q˙P˙t˙W
14 cdleme27.o O=P˙Q˙Z˙t˙z˙W
15 cdleme27.e E=ιuB|zA¬z˙W¬z˙P˙Qu=O
16 cdleme27.y Y=ift˙P˙QEG
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdleme27b s=tC=Y
18 17 adantl KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Ws=tC=Y
19 simp11l KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WKHL
20 19 hllatd KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WKLat
21 simp11r KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WWH
22 simp21 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WPA¬P˙W
23 simp22 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WQA¬Q˙W
24 simp23 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WtA¬t˙W
25 simp12 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WPQ
26 1 2 3 4 5 6 7 13 9 14 15 16 cdleme27cl KHLWHPA¬P˙WQA¬Q˙WtA¬t˙WPQYB
27 19 21 22 23 24 25 26 syl222anc KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WYB
28 simp3rl KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WVA
29 1 5 atbase VAVB
30 28 29 syl KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WVB
31 1 2 3 latlej1 KLatYBVBY˙Y˙V
32 20 27 30 31 syl3anc KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WY˙Y˙V
33 32 adantr KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Ws=tY˙Y˙V
34 18 33 eqbrtrd KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Ws=tC˙Y˙V
35 simpl11 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstKHLWH
36 simpl12 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstPQ
37 simpl13 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstsA¬s˙W
38 simpl21 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstPA¬P˙W
39 simpl22 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstQA¬Q˙W
40 simpl23 KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WsttA¬t˙W
41 simpr KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Wstst
42 simpl3l KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Wsts˙t˙V
43 41 42 jca KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙Wststs˙t˙V
44 simpl3r KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstVAV˙W
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdleme27a KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Wsts˙t˙VVAV˙WC˙Y˙V
46 35 36 37 38 39 40 43 44 45 syl332anc KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WstC˙Y˙V
47 34 46 pm2.61dane KHLWHPQsA¬s˙WPA¬P˙WQA¬Q˙WtA¬t˙Ws˙t˙VVAV˙WC˙Y˙V