Metamath Proof Explorer

Theorem cdlemi1

Description: Part of proof of Lemma I of Crawley p. 118. (Contributed by NM, 18-Jun-2013)

Ref Expression
Hypotheses cdlemi.b ⊢ B = Base K
cdlemi.l ⊢ ≤ ˙ = ≤ K
cdlemi.j ⊢ ∨ ˙ = join ⁡ K
cdlemi.m ⊢ ∧ ˙ = meet ⁡ K
cdlemi.a ⊢ A = Atoms ⁡ K
cdlemi.h ⊢ H = LHyp ⁡ K
cdlemi.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemi.r ⊢ R = trL ⁡ K ⁡ W
cdlemi.e ⊢ E = TEndo ⁡ K ⁡ W
Assertion cdlemi1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ⁡ P ≤ ˙ P ∨ ˙ R ⁡ G

Proof

Step Hyp Ref Expression
1 cdlemi.b ⊢ B = Base K
2 cdlemi.l ⊢ ≤ ˙ = ≤ K
3 cdlemi.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemi.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemi.a ⊢ A = Atoms ⁡ K
6 cdlemi.h ⊢ H = LHyp ⁡ K
7 cdlemi.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemi.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemi.e ⊢ E = TEndo ⁡ K ⁡ W
10 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL
11 10 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ Lat
12 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL ∧ W ∈ H
13 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ∈ E
14 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ∈ T
15 6 7 9 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T → U ⁡ G ∈ T
16 12 13 14 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ∈ T
17 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ A
18 1 5 atbase ⊢ P ∈ A → P ∈ B
19 17 18 syl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ B
20 1 6 7 ltrncl ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ G ∈ T ∧ P ∈ B → U ⁡ G ⁡ P ∈ B
21 12 16 19 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ⁡ P ∈ B
22 1 6 7 8 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ G ∈ T → R ⁡ U ⁡ G ∈ B
23 12 16 22 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ U ⁡ G ∈ B
24 1 3 latjcl ⊢ K ∈ Lat ∧ P ∈ B ∧ R ⁡ U ⁡ G ∈ B → P ∨ ˙ R ⁡ U ⁡ G ∈ B
25 11 19 23 24 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ U ⁡ G ∈ B
26 1 6 7 8 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T → R ⁡ G ∈ B
27 12 14 26 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ G ∈ B
28 1 3 latjcl ⊢ K ∈ Lat ∧ P ∈ B ∧ R ⁡ G ∈ B → P ∨ ˙ R ⁡ G ∈ B
29 11 19 27 28 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ G ∈ B
30 1 2 3 latlej2 ⊢ K ∈ Lat ∧ P ∈ B ∧ U ⁡ G ⁡ P ∈ B → U ⁡ G ⁡ P ≤ ˙ P ∨ ˙ U ⁡ G ⁡ P
31 11 19 21 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ⁡ P ≤ ˙ P ∨ ˙ U ⁡ G ⁡ P
32 2 3 4 5 6 7 8 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ U ⁡ G = P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ W
33 16 32 syld3an2 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ U ⁡ G = P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ W
34 33 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ U ⁡ G = P ∨ ˙ P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ W
35 1 3 latjcl ⊢ K ∈ Lat ∧ P ∈ B ∧ U ⁡ G ⁡ P ∈ B → P ∨ ˙ U ⁡ G ⁡ P ∈ B
36 11 19 21 35 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ U ⁡ G ⁡ P ∈ B
37 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ H
38 1 6 lhpbase ⊢ W ∈ H → W ∈ B
39 37 38 syl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ B
40 1 2 3 latlej1 ⊢ K ∈ Lat ∧ P ∈ B ∧ U ⁡ G ⁡ P ∈ B → P ≤ ˙ P ∨ ˙ U ⁡ G ⁡ P
41 11 19 21 40 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≤ ˙ P ∨ ˙ U ⁡ G ⁡ P
42 1 2 3 4 5 atmod3i1 ⊢ K ∈ HL ∧ P ∈ A ∧ P ∨ ˙ U ⁡ G ⁡ P ∈ B ∧ W ∈ B ∧ P ≤ ˙ P ∨ ˙ U ⁡ G ⁡ P → P ∨ ˙ P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ P ∨ ˙ W
43 10 17 36 39 41 42 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ W = P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ P ∨ ˙ W
44 eqid ⊢ 1. ⁡ K = 1. ⁡ K
45 2 3 44 5 6 lhpjat2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1. ⁡ K
46 45 3adant2 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1. ⁡ K
47 46 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ P ∨ ˙ W = P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ 1. ⁡ K
48 hlol ⊢ K ∈ HL → K ∈ OL
49 10 48 syl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ OL
50 1 4 44 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ U ⁡ G ⁡ P ∈ B → P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ 1. ⁡ K = P ∨ ˙ U ⁡ G ⁡ P
51 49 36 50 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ 1. ⁡ K = P ∨ ˙ U ⁡ G ⁡ P
52 47 51 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ U ⁡ G ⁡ P ∧ ˙ P ∨ ˙ W = P ∨ ˙ U ⁡ G ⁡ P
53 34 43 52 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ U ⁡ G = P ∨ ˙ U ⁡ G ⁡ P
54 31 53 breqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ⁡ P ≤ ˙ P ∨ ˙ R ⁡ U ⁡ G
55 2 6 7 8 9 tendotp ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T → R ⁡ U ⁡ G ≤ ˙ R ⁡ G
56 12 13 14 55 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ U ⁡ G ≤ ˙ R ⁡ G
57 1 2 3 latjlej2 ⊢ K ∈ Lat ∧ R ⁡ U ⁡ G ∈ B ∧ R ⁡ G ∈ B ∧ P ∈ B → R ⁡ U ⁡ G ≤ ˙ R ⁡ G → P ∨ ˙ R ⁡ U ⁡ G ≤ ˙ P ∨ ˙ R ⁡ G
58 11 23 27 19 57 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ U ⁡ G ≤ ˙ R ⁡ G → P ∨ ˙ R ⁡ U ⁡ G ≤ ˙ P ∨ ˙ R ⁡ G
59 56 58 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ U ⁡ G ≤ ˙ P ∨ ˙ R ⁡ G
60 1 2 11 21 25 29 54 59 lattrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → U ⁡ G ⁡ P ≤ ˙ P ∨ ˙ R ⁡ G