Metamath Proof Explorer

Theorem cdlemg8b

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013)

Ref Expression
Hypotheses cdlemg8.l ⊢ ≤ ˙ = ≤ K
cdlemg8.j ⊢ ∨ ˙ = join ⁡ K
cdlemg8.m ⊢ ∧ ˙ = meet ⁡ K
cdlemg8.a ⊢ A = Atoms ⁡ K
cdlemg8.h ⊢ H = LHyp ⁡ K
cdlemg8.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion cdlemg8b ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 cdlemg8.l ⊢ ≤ ˙ = ≤ K
2 cdlemg8.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemg8.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemg8.a ⊢ A = Atoms ⁡ K
5 cdlemg8.h ⊢ H = LHyp ⁡ K
6 cdlemg8.t ⊢ T = LTrn ⁡ K ⁡ W
7 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → K ∈ HL
8 7 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → K ∈ Lat
9 simp21l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∈ A
10 eqid ⊢ Base K = Base K
11 10 4 atbase ⊢ P ∈ A → P ∈ Base K
12 9 11 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∈ Base K
13 simp22l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → Q ∈ A
14 10 4 atbase ⊢ Q ∈ A → Q ∈ Base K
15 13 14 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → Q ∈ Base K
16 10 1 2 latlej1 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ≤ ˙ P ∨ ˙ Q
17 8 12 15 16 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ≤ ˙ P ∨ ˙ Q
18 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → K ∈ HL ∧ W ∈ H
19 simp23 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ∈ T
20 simp31 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → G ∈ T
21 simp21 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∈ A ∧ ¬ P ≤ ˙ W
22 1 4 5 6 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
23 18 20 21 22 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
24 1 4 5 6 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W → F ⁡ G ⁡ P ∈ A ∧ ¬ F ⁡ G ⁡ P ≤ ˙ W
25 24 simpld ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W → F ⁡ G ⁡ P ∈ A
26 18 19 23 25 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ∈ A
27 10 4 atbase ⊢ F ⁡ G ⁡ P ∈ A → F ⁡ G ⁡ P ∈ Base K
28 26 27 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ∈ Base K
29 10 5 6 ltrncl ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ Q ∈ Base K → G ⁡ Q ∈ Base K
30 18 20 15 29 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → G ⁡ Q ∈ Base K
31 10 5 6 ltrncl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ Q ∈ Base K → F ⁡ G ⁡ Q ∈ Base K
32 18 19 30 31 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ Q ∈ Base K
33 10 1 2 latlej1 ⊢ K ∈ Lat ∧ F ⁡ G ⁡ P ∈ Base K ∧ F ⁡ G ⁡ Q ∈ Base K → F ⁡ G ⁡ P ≤ ˙ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q
34 8 28 32 33 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ≤ ˙ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q
35 simp32 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q
36 34 35 breqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q
37 10 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
38 7 9 13 37 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ Q ∈ Base K
39 10 1 2 latjle12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ F ⁡ G ⁡ P ∈ Base K ∧ P ∨ ˙ Q ∈ Base K → P ≤ ˙ P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q
40 8 12 28 38 39 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ≤ ˙ P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q
41 17 36 40 mpbi2and ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q
42 simp33 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → F ⁡ G ⁡ P ≠ P
43 42 necomd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ≠ F ⁡ G ⁡ P
44 1 2 4 ps-1 ⊢ K ∈ HL ∧ P ∈ A ∧ F ⁡ G ⁡ P ∈ A ∧ P ≠ F ⁡ G ⁡ P ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ Q
45 7 9 26 43 9 13 44 syl132anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P ≤ ˙ P ∨ ˙ Q ↔ P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ Q
46 41 45 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T ∧ G ∈ T ∧ F ⁡ G ⁡ P ∨ ˙ F ⁡ G ⁡ Q = P ∨ ˙ Q ∧ F ⁡ G ⁡ P ≠ P → P ∨ ˙ F ⁡ G ⁡ P = P ∨ ˙ Q