Metamath Proof Explorer

Theorem cdlemg2m

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

Ref Expression
Hypotheses cdlemg2inv.h ⊢ H = LHyp ⁡ K
cdlemg2inv.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemg2j.l ⊢ ≤ ˙ = ≤ K
cdlemg2j.j ⊢ ∨ ˙ = join ⁡ K
cdlemg2j.a ⊢ A = Atoms ⁡ K
cdlemg2j.m ⊢ ∧ ˙ = meet ⁡ K
cdlemg2j.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
Assertion cdlemg2m ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ F ⁡ Q ∧ ˙ W = U

Proof

Step Hyp Ref Expression
1 cdlemg2inv.h ⊢ H = LHyp ⁡ K
2 cdlemg2inv.t ⊢ T = LTrn ⁡ K ⁡ W
3 cdlemg2j.l ⊢ ≤ ˙ = ≤ K
4 cdlemg2j.j ⊢ ∨ ˙ = join ⁡ K
5 cdlemg2j.a ⊢ A = Atoms ⁡ K
6 cdlemg2j.m ⊢ ∧ ˙ = meet ⁡ K
7 cdlemg2j.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
8 1 2 3 4 5 6 7 cdlemg2k ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ F ⁡ Q = F ⁡ P ∨ ˙ U
9 8 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ F ⁡ Q ∧ ˙ W = F ⁡ P ∨ ˙ U ∧ ˙ W
10 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → K ∈ HL ∧ W ∈ H
11 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ∈ T
12 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → P ∈ A ∧ ¬ P ≤ ˙ W
13 eqid ⊢ 0. ⁡ K = 0. ⁡ K
14 3 6 13 5 1 2 ltrnmw ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ P ∧ ˙ W = 0. ⁡ K
15 10 11 12 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∧ ˙ W = 0. ⁡ K
16 15 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∧ ˙ W ∨ ˙ U = 0. ⁡ K ∨ ˙ U
17 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → K ∈ HL
18 3 5 1 2 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
19 10 11 12 18 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
20 19 simpld ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∈ A
21 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → W ∈ H
22 simp2ll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → P ∈ A
23 simp2rl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → Q ∈ A
24 eqid ⊢ Base K = Base K
25 3 4 6 5 1 7 24 cdleme0aa ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A → U ∈ Base K
26 17 21 22 23 25 syl211anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → U ∈ Base K
27 24 1 lhpbase ⊢ W ∈ H → W ∈ Base K
28 21 27 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → W ∈ Base K
29 17 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → K ∈ Lat
30 24 4 5 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
31 17 22 23 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → P ∨ ˙ Q ∈ Base K
32 24 3 6 latmle2 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → P ∨ ˙ Q ∧ ˙ W ≤ ˙ W
33 29 31 28 32 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → P ∨ ˙ Q ∧ ˙ W ≤ ˙ W
34 7 33 eqbrtrid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → U ≤ ˙ W
35 24 3 4 6 5 atmod4i2 ⊢ K ∈ HL ∧ F ⁡ P ∈ A ∧ U ∈ Base K ∧ W ∈ Base K ∧ U ≤ ˙ W → F ⁡ P ∧ ˙ W ∨ ˙ U = F ⁡ P ∨ ˙ U ∧ ˙ W
36 17 20 26 28 34 35 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∧ ˙ W ∨ ˙ U = F ⁡ P ∨ ˙ U ∧ ˙ W
37 hlol ⊢ K ∈ HL → K ∈ OL
38 17 37 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → K ∈ OL
39 24 4 13 olj02 ⊢ K ∈ OL ∧ U ∈ Base K → 0. ⁡ K ∨ ˙ U = U
40 38 26 39 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → 0. ⁡ K ∨ ˙ U = U
41 16 36 40 3eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ U ∧ ˙ W = U
42 9 41 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ F ∈ T → F ⁡ P ∨ ˙ F ⁡ Q ∧ ˙ W = U