Metamath Proof Explorer


Theorem cdleme13

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, " and are centrally perspective." F and G represent f(s) and f(t) respectively. (Contributed by NM, 7-Oct-2012)

Ref Expression
Hypotheses cdleme12.l ˙ = K
cdleme12.j ˙ = join K
cdleme12.m ˙ = meet K
cdleme12.a A = Atoms K
cdleme12.h H = LHyp K
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 cdleme13 K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T S ˙ F ˙ T ˙ G ˙ P ˙ Q

Proof

Step Hyp Ref Expression
1 cdleme12.l ˙ = K
2 cdleme12.j ˙ = join K
3 cdleme12.m ˙ = meet K
4 cdleme12.a A = Atoms K
5 cdleme12.h H = LHyp K
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 1 2 3 4 5 6 7 8 cdleme12 K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T S ˙ F ˙ T ˙ G = U
10 9 6 eqtrdi K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T S ˙ F ˙ T ˙ G = P ˙ Q ˙ W
11 simp1l K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T K HL
12 11 hllatd K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T K Lat
13 simp21l K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T P A
14 simp22 K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T Q A
15 eqid Base K = Base K
16 15 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
17 11 13 14 16 syl3anc K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T P ˙ Q Base K
18 simp1r K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T W H
19 15 5 lhpbase W H W Base K
20 18 19 syl K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T W Base K
21 15 1 3 latmle1 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ P ˙ Q
22 12 17 20 21 syl3anc K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T P ˙ Q ˙ W ˙ P ˙ Q
23 10 22 eqbrtrd K HL W H P A ¬ P ˙ W Q A P Q S A ¬ S ˙ W T A ¬ T ˙ W S T ¬ U ˙ S ˙ T S ˙ F ˙ T ˙ G ˙ P ˙ Q