Metamath Proof Explorer


Theorem cdleme11

Description: Part of proof of Lemma E in Crawley p. 113, 1st sentence of 3rd paragraph on p. 114. F and G represent f(s) and f(t) respectively. Their proof provides no details of our cdleme11a through cdleme11 , so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-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 cdleme11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G = S ˙ T

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 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T K HL
10 9 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T K Lat
11 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T K HL W H
12 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T P A
13 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T Q A
14 eqid Base K = Base K
15 1 2 3 4 5 6 14 cdleme0aa K HL W H P A Q A U Base K
16 11 12 13 15 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T U Base K
17 14 2 latjidm K Lat U Base K U ˙ U = U
18 10 16 17 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T U ˙ U = U
19 18 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T ˙ U ˙ U = S ˙ T ˙ U
20 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T U ˙ S ˙ T
21 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S A
22 14 4 atbase S A S Base K
23 21 22 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S Base K
24 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T T A
25 14 4 atbase T A T Base K
26 24 25 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T T Base K
27 14 2 latjcl K Lat S Base K T Base K S ˙ T Base K
28 10 23 26 27 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T Base K
29 14 1 2 latleeqj2 K Lat U Base K S ˙ T Base K U ˙ S ˙ T S ˙ T ˙ U = S ˙ T
30 10 16 28 29 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T U ˙ S ˙ T S ˙ T ˙ U = S ˙ T
31 20 30 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T ˙ U = S ˙ T
32 19 31 eqtr2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T = S ˙ T ˙ U ˙ U
33 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S A ¬ S ˙ W
34 1 2 3 4 5 6 7 cdleme1 K HL W H P A Q A S A ¬ S ˙ W S ˙ F = S ˙ U
35 11 12 13 33 34 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ F = S ˙ U
36 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T T A ¬ T ˙ W
37 1 2 3 4 5 6 8 cdleme1 K HL W H P A Q A T A ¬ T ˙ W T ˙ G = T ˙ U
38 11 12 13 36 37 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T T ˙ G = T ˙ U
39 35 38 oveq12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ F ˙ T ˙ G = S ˙ U ˙ T ˙ U
40 14 2 latj4 K Lat S Base K T Base K U Base K U Base K S ˙ T ˙ U ˙ U = S ˙ U ˙ T ˙ U
41 10 23 26 16 16 40 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T ˙ U ˙ U = S ˙ U ˙ T ˙ U
42 39 41 eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ F ˙ T ˙ G = S ˙ T ˙ U ˙ U
43 32 42 eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T = S ˙ F ˙ T ˙ G
44 1 2 3 4 5 6 7 14 cdleme1b K HL W H P A Q A S A F Base K
45 11 12 13 21 44 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F Base K
46 1 2 3 4 5 6 8 14 cdleme1b K HL W H P A Q A T A G Base K
47 11 12 13 24 46 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T G Base K
48 14 2 latj4 K Lat S Base K F Base K T Base K G Base K S ˙ F ˙ T ˙ G = S ˙ T ˙ F ˙ G
49 10 23 45 26 47 48 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ F ˙ T ˙ G = S ˙ T ˙ F ˙ G
50 43 49 eqtr2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T S ˙ T ˙ F ˙ G = S ˙ T
51 14 2 latjcl K Lat F Base K G Base K F ˙ G Base K
52 10 45 47 51 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G Base K
53 14 1 2 latleeqj2 K Lat F ˙ G Base K S ˙ T Base K F ˙ G ˙ S ˙ T S ˙ T ˙ F ˙ G = S ˙ T
54 10 52 28 53 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G ˙ S ˙ T S ˙ T ˙ F ˙ G = S ˙ T
55 50 54 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G ˙ S ˙ T
56 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T P A ¬ P ˙ W
57 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T Q A ¬ Q ˙ W
58 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T P Q
59 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T ¬ S ˙ P ˙ Q
60 1 2 3 4 5 6 7 cdleme3fa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F A
61 11 56 57 33 58 59 60 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F A
62 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T ¬ T ˙ P ˙ Q
63 1 2 3 4 5 6 8 cdleme3fa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W P Q ¬ T ˙ P ˙ Q G A
64 11 56 57 36 58 62 63 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T G A
65 1 2 3 4 5 6 7 8 cdleme11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F G
66 1 2 4 ps-1 K HL F A G A F G S A T A F ˙ G ˙ S ˙ T F ˙ G = S ˙ T
67 9 61 64 65 21 24 66 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G ˙ S ˙ T F ˙ G = S ˙ T
68 55 67 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q U ˙ S ˙ T F ˙ G = S ˙ T