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 = Base K
cdleme26.l ˙ = K
cdleme26.j ˙ = join K
cdleme26.m ˙ = meet K
cdleme26.a A = Atoms K
cdleme26.h H = LHyp K
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 = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
cdleme27.c C = if s ˙ P ˙ Q D F
cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
cdleme27.y Y = if t ˙ P ˙ Q E G
Assertion cdleme27N K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W C ˙ Y ˙ V

Proof

Step Hyp Ref Expression
1 cdleme26.b B = Base K
2 cdleme26.l ˙ = K
3 cdleme26.j ˙ = join K
4 cdleme26.m ˙ = meet K
5 cdleme26.a A = Atoms K
6 cdleme26.h H = LHyp K
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 = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
12 cdleme27.c C = if s ˙ P ˙ Q D F
13 cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
14 cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
15 cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
16 cdleme27.y Y = if t ˙ P ˙ Q E G
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdleme27b s = t C = Y
18 17 adantl K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s = t C = Y
19 simp11l K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W K HL
20 19 hllatd K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W K Lat
21 simp11r K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W W H
22 simp21 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W P A ¬ P ˙ W
23 simp22 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W Q A ¬ Q ˙ W
24 simp23 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W t A ¬ t ˙ W
25 simp12 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W P Q
26 1 2 3 4 5 6 7 13 9 14 15 16 cdleme27cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W P Q Y B
27 19 21 22 23 24 25 26 syl222anc K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W Y B
28 simp3rl K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W V A
29 1 5 atbase V A V B
30 28 29 syl K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W V B
31 1 2 3 latlej1 K Lat Y B V B Y ˙ Y ˙ V
32 20 27 30 31 syl3anc K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W Y ˙ Y ˙ V
33 32 adantr K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s = t Y ˙ Y ˙ V
34 18 33 eqbrtrd K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s = t C ˙ Y ˙ V
35 simpl11 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t K HL W H
36 simpl12 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t P Q
37 simpl13 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t s A ¬ s ˙ W
38 simpl21 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t P A ¬ P ˙ W
39 simpl22 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t Q A ¬ Q ˙ W
40 simpl23 K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t t A ¬ t ˙ W
41 simpr K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t s t
42 simpl3l K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t s ˙ t ˙ V
43 41 42 jca K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t s t s ˙ t ˙ V
44 simpl3r K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t V A V ˙ W
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdleme27a K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s t s ˙ t ˙ V V A V ˙ W C ˙ Y ˙ V
46 35 36 37 38 39 40 43 44 45 syl332anc K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W s t C ˙ Y ˙ V
47 34 46 pm2.61dane K HL W H P Q s A ¬ s ˙ W P A ¬ P ˙ W Q A ¬ Q ˙ W t A ¬ t ˙ W s ˙ t ˙ V V A V ˙ W C ˙ Y ˙ V