Metamath Proof Explorer


Theorem cdlemd4

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemd4.l ˙ = K
cdlemd4.j ˙ = join K
cdlemd4.a A = Atoms K
cdlemd4.h H = LHyp K
cdlemd4.t T = LTrn K W
Assertion cdlemd4 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q F R = G R

Proof

Step Hyp Ref Expression
1 cdlemd4.l ˙ = K
2 cdlemd4.j ˙ = join K
3 cdlemd4.a A = Atoms K
4 cdlemd4.h H = LHyp K
5 cdlemd4.t T = LTrn K W
6 simp11l K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q K HL
7 simp11r K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q W H
8 simp21 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q P A ¬ P ˙ W
9 simp22 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q Q A ¬ Q ˙ W
10 simp231 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q P Q
11 1 2 3 4 cdlemb2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q
12 6 7 8 9 10 11 syl221anc K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q
13 simpl11 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q K HL W H
14 simpl12 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q F T G T
15 simpl13 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q R A
16 simpl21 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P A ¬ P ˙ W
17 simprl K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s A
18 simprrl K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ s ˙ W
19 17 18 jca K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s A ¬ s ˙ W
20 6 hllatd K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q K Lat
21 20 adantr K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q K Lat
22 eqid Base K = Base K
23 22 3 atbase s A s Base K
24 23 ad2antrl K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s Base K
25 simp21l K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q P A
26 22 3 atbase P A P Base K
27 25 26 syl K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q P Base K
28 27 adantr K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Base K
29 simp22l K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q Q A
30 22 3 atbase Q A Q Base K
31 29 30 syl K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q Q Base K
32 31 adantr K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q Q Base K
33 simprrr K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ s ˙ P ˙ Q
34 22 1 2 latnlej1l K Lat s Base K P Base K Q Base K ¬ s ˙ P ˙ Q s P
35 34 necomd K Lat s Base K P Base K Q Base K ¬ s ˙ P ˙ Q P s
36 21 24 28 32 33 35 syl131anc K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P s
37 simpl22 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q Q A ¬ Q ˙ W
38 simpl23 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Q R ˙ P ˙ Q R P
39 1 2 3 4 cdlemd3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P R A s A ¬ s ˙ P ˙ Q ¬ R ˙ P ˙ s
40 13 16 37 38 15 17 33 39 syl133anc K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ R ˙ P ˙ s
41 36 40 jca K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P s ¬ R ˙ P ˙ s
42 simpl3l K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q F P = G P
43 10 adantr K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Q
44 43 33 jca K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Q ¬ s ˙ P ˙ Q
45 simpl3 K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q F P = G P F Q = G Q
46 1 2 3 4 5 cdlemd2 K HL W H F T G T s A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ s ˙ P ˙ Q F P = G P F Q = G Q F s = G s
47 13 14 17 16 37 44 45 46 syl331anc K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q F s = G s
48 1 2 3 4 5 cdlemd2 K HL W H F T G T R A P A ¬ P ˙ W s A ¬ s ˙ W P s ¬ R ˙ P ˙ s F P = G P F s = G s F R = G R
49 13 14 15 16 19 41 42 47 48 syl332anc K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q F R = G R
50 12 49 rexlimddv K HL W H F T G T R A P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R ˙ P ˙ Q R P F P = G P F Q = G Q F R = G R