Metamath Proof Explorer

Theorem cdlemg17a

Description: TODO: FIX COMMENT. (Contributed by NM, 8-May-2013)

Ref Expression
Hypotheses cdlemg12.l ⊢ ≤ ˙ = ≤ K
cdlemg12.j ⊢ ∨ ˙ = join ⁡ K
cdlemg12.m ⊢ ∧ ˙ = meet ⁡ K
cdlemg12.a ⊢ A = Atoms ⁡ K
cdlemg12.h ⊢ H = LHyp ⁡ K
cdlemg12.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemg12b.r ⊢ R = trL ⁡ K ⁡ W
Assertion cdlemg17a ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ⁡ P ≤ ˙ P ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 cdlemg12.l ⊢ ≤ ˙ = ≤ K
2 cdlemg12.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemg12.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemg12.a ⊢ A = Atoms ⁡ K
5 cdlemg12.h ⊢ H = LHyp ⁡ K
6 cdlemg12.t ⊢ T = LTrn ⁡ K ⁡ W
7 cdlemg12b.r ⊢ R = trL ⁡ K ⁡ W
8 eqid ⊢ Base K = Base K
9 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → K ∈ HL
10 9 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → K ∈ Lat
11 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → K ∈ HL ∧ W ∈ H
12 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ∈ T
13 simp2ll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∈ A
14 1 4 5 6 ltrnat ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A → G ⁡ P ∈ A
15 11 12 13 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ⁡ P ∈ A
16 8 4 atbase ⊢ G ⁡ P ∈ A → G ⁡ P ∈ Base K
17 15 16 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ⁡ P ∈ Base K
18 8 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ G ⁡ P ∈ A → P ∨ ˙ G ⁡ P ∈ Base K
19 9 13 15 18 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ G ⁡ P ∈ Base K
20 simp2rl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → Q ∈ A
21 8 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
22 9 13 20 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ Q ∈ Base K
23 1 2 4 hlatlej2 ⊢ K ∈ HL ∧ P ∈ A ∧ G ⁡ P ∈ A → G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P
24 9 13 15 23 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ⁡ P ≤ ˙ P ∨ ˙ G ⁡ P
25 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∈ A ∧ ¬ P ≤ ˙ W
26 eqid ⊢ P ∨ ˙ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P ∧ ˙ W
27 1 2 3 4 5 26 cdleme0cp ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ G ⁡ P ∈ A → P ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P
28 11 25 15 27 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W = P ∨ ˙ G ⁡ P
29 1 2 4 hlatlej1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≤ ˙ P ∨ ˙ Q
30 9 13 20 29 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ≤ ˙ P ∨ ˙ Q
31 1 2 3 4 5 6 7 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ G = P ∨ ˙ G ⁡ P ∧ ˙ W
32 11 12 25 31 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → R ⁡ G = P ∨ ˙ G ⁡ P ∧ ˙ W
33 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → R ⁡ G ≤ ˙ P ∨ ˙ Q
34 32 33 eqbrtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q
35 8 4 atbase ⊢ P ∈ A → P ∈ Base K
36 13 35 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∈ Base K
37 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → W ∈ H
38 8 5 lhpbase ⊢ W ∈ H → W ∈ Base K
39 37 38 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → W ∈ Base K
40 8 3 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ G ⁡ P ∈ Base K ∧ W ∈ Base K → P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K
41 10 19 39 40 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K
42 8 1 2 latjle12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ∈ Base K ∧ P ∨ ˙ Q ∈ Base K → P ≤ ˙ P ∨ ˙ Q ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q
43 10 36 41 22 42 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ≤ ˙ P ∨ ˙ Q ∧ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q
44 30 34 43 mpbi2and ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ P ∨ ˙ G ⁡ P ∧ ˙ W ≤ ˙ P ∨ ˙ Q
45 28 44 eqbrtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → P ∨ ˙ G ⁡ P ≤ ˙ P ∨ ˙ Q
46 8 1 10 17 19 22 24 45 lattrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ G ∈ T ∧ R ⁡ G ≤ ˙ P ∨ ˙ Q → G ⁡ P ≤ ˙ P ∨ ˙ Q