Metamath Proof Explorer


Theorem cdleme37m

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013)

Ref Expression
Hypotheses cdleme37.l ˙=K
cdleme37.j ˙=joinK
cdleme37.m ˙=meetK
cdleme37.a A=AtomsK
cdleme37.h H=LHypK
cdleme37.u U=P˙Q˙W
cdleme37.e E=t˙U˙Q˙P˙t˙W
cdleme37.d D=u˙U˙Q˙P˙u˙W
cdleme37.v V=t˙E˙W
cdleme37.x X=u˙D˙W
cdleme37.c C=S˙V˙E˙t˙S˙W
cdleme37.g G=S˙X˙D˙u˙S˙W
Assertion cdleme37m KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QC=G

Proof

Step Hyp Ref Expression
1 cdleme37.l ˙=K
2 cdleme37.j ˙=joinK
3 cdleme37.m ˙=meetK
4 cdleme37.a A=AtomsK
5 cdleme37.h H=LHypK
6 cdleme37.u U=P˙Q˙W
7 cdleme37.e E=t˙U˙Q˙P˙t˙W
8 cdleme37.d D=u˙U˙Q˙P˙u˙W
9 cdleme37.v V=t˙E˙W
10 cdleme37.x X=u˙D˙W
11 cdleme37.c C=S˙V˙E˙t˙S˙W
12 cdleme37.g G=S˙X˙D˙u˙S˙W
13 simp1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QKHLWHPA¬P˙WQA¬Q˙W
14 simp23 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QSA¬S˙W
15 simp32l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QtA¬t˙W
16 simp33l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QuA¬u˙W
17 simp21 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QPQ
18 simp32r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙Q¬t˙P˙Q
19 simp33r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙Q¬u˙P˙Q
20 simp31r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙P˙Q
21 18 19 20 3jca KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙Q¬t˙P˙Q¬u˙P˙QS˙P˙Q
22 eqid S˙t˙W=S˙t˙W
23 eqid S˙u˙W=S˙u˙W
24 eqid P˙Q˙E˙S˙t˙W=P˙Q˙E˙S˙t˙W
25 eqid P˙Q˙D˙S˙u˙W=P˙Q˙D˙S˙u˙W
26 1 2 3 4 5 6 7 8 22 23 24 25 cdleme21k KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WtA¬t˙WuA¬u˙WPQ¬t˙P˙Q¬u˙P˙QS˙P˙QP˙Q˙E˙S˙t˙W=P˙Q˙D˙S˙u˙W
27 13 14 15 16 17 21 26 syl132anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q˙E˙S˙t˙W=P˙Q˙D˙S˙u˙W
28 simp11 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QKHLWH
29 simp12l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QPA
30 simp13l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QQA
31 1 2 3 4 5 6 cdleme4 KHLWHPAQASA¬S˙WS˙P˙QP˙Q=S˙U
32 28 29 30 14 20 31 syl131anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q=S˙U
33 1 2 3 4 5 6 7 cdleme2 KHLWHPAQAtA¬t˙Wt˙E˙W=U
34 28 29 30 15 33 syl13anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙Qt˙E˙W=U
35 9 34 eqtrid KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QV=U
36 35 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙V=S˙U
37 32 36 eqtr4d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q=S˙V
38 simp11l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QKHL
39 simp23l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QSA
40 15 simpld KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QtA
41 2 4 hlatjcom KHLSAtAS˙t=t˙S
42 38 39 40 41 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙t=t˙S
43 42 oveq1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙t˙W=t˙S˙W
44 43 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QE˙S˙t˙W=E˙t˙S˙W
45 37 44 oveq12d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q˙E˙S˙t˙W=S˙V˙E˙t˙S˙W
46 11 45 eqtr4id KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QC=P˙Q˙E˙S˙t˙W
47 1 2 3 4 5 6 8 cdleme2 KHLWHPAQAuA¬u˙Wu˙D˙W=U
48 28 29 30 16 47 syl13anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙Qu˙D˙W=U
49 10 48 eqtrid KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QX=U
50 49 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙X=S˙U
51 32 50 eqtr4d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q=S˙X
52 16 simpld KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QuA
53 2 4 hlatjcom KHLSAuAS˙u=u˙S
54 38 39 52 53 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙u=u˙S
55 54 oveq1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QS˙u˙W=u˙S˙W
56 55 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QD˙S˙u˙W=D˙u˙S˙W
57 51 56 oveq12d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QP˙Q˙D˙S˙u˙W=S˙X˙D˙u˙S˙W
58 12 57 eqtr4id KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QG=P˙Q˙D˙S˙u˙W
59 27 46 58 3eqtr4d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙QS˙P˙QtA¬t˙W¬t˙P˙QuA¬u˙W¬u˙P˙QC=G