Metamath Proof Explorer


Theorem cdleme11l

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 15-Jun-2012)

Ref Expression
Hypotheses cdleme12.l ˙=K
cdleme12.j ˙=joinK
cdleme12.m ˙=meetK
cdleme12.a A=AtomsK
cdleme12.h H=LHypK
cdleme12.u U=P˙Q˙W
cdleme12.f F=S˙U˙Q˙P˙S˙W
cdleme12.g G=T˙U˙Q˙P˙T˙W
Assertion cdleme11l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TFG

Proof

Step Hyp Ref Expression
1 cdleme12.l ˙=K
2 cdleme12.j ˙=joinK
3 cdleme12.m ˙=meetK
4 cdleme12.a A=AtomsK
5 cdleme12.h H=LHypK
6 cdleme12.u U=P˙Q˙W
7 cdleme12.f F=S˙U˙Q˙P˙S˙W
8 cdleme12.g G=T˙U˙Q˙P˙T˙W
9 simp11 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TKHLWH
10 simp12 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TPA¬P˙W
11 simp13l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TQA
12 simp21 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TSA¬S˙W
13 simp22l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TTA
14 simp23l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TPQ
15 simp23r KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TST
16 simp31 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙T¬S˙P˙Q
17 simp33 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TU˙S˙T
18 eqid P˙S˙W=P˙S˙W
19 eqid P˙T˙W=P˙T˙W
20 1 2 3 4 5 6 18 19 cdleme11e KHLWHPA¬P˙WQASA¬S˙WTAPQST¬S˙P˙QU˙S˙TP˙S˙WP˙T˙W
21 9 10 11 12 13 14 15 16 17 20 syl333anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TP˙S˙WP˙T˙W
22 oveq2 F=GQ˙F=Q˙G
23 22 oveq1d F=GQ˙F˙W=Q˙G˙W
24 23 adantl KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TF=GQ˙F˙W=Q˙G˙W
25 simp13 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TQA¬Q˙W
26 1 2 3 4 5 6 18 6 7 cdleme11k KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QP˙S˙W=Q˙F˙W
27 9 10 25 12 14 16 26 syl132anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TP˙S˙W=Q˙F˙W
28 27 adantr KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TF=GP˙S˙W=Q˙F˙W
29 simp22 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TTA¬T˙W
30 simp32 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙T¬T˙P˙Q
31 1 2 3 4 5 6 19 6 8 cdleme11k KHLWHPA¬P˙WQA¬Q˙WTA¬T˙WPQ¬T˙P˙QP˙T˙W=Q˙G˙W
32 9 10 25 29 14 30 31 syl132anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TP˙T˙W=Q˙G˙W
33 32 adantr KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TF=GP˙T˙W=Q˙G˙W
34 24 28 33 3eqtr4d KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TF=GP˙S˙W=P˙T˙W
35 34 ex KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TF=GP˙S˙W=P˙T˙W
36 35 necon3d KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TP˙S˙WP˙T˙WFG
37 21 36 mpd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QU˙S˙TFG