Metamath Proof Explorer

Theorem 4atlem11a

Description: Lemma for 4at . Substitute U for Q . (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l ⊢ ≤ ˙ = ≤ K
4at.j ⊢ ∨ ˙ = join ⁡ K
4at.a ⊢ A = Atoms ⁡ K
Assertion 4atlem11a ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ≤ ˙ P ∨ ˙ U ∨ ˙ V ∨ ˙ W ↔ P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = P ∨ ˙ U ∨ ˙ V ∨ ˙ W

Proof

Step Hyp Ref Expression
1 4at.l ⊢ ≤ ˙ = ≤ K
2 4at.j ⊢ ∨ ˙ = join ⁡ K
3 4at.a ⊢ A = Atoms ⁡ K
4 simp11 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → K ∈ HL
5 simp13 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ∈ A
6 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → U ∈ A
7 4 hllatd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → K ∈ Lat
8 simp12 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∈ A
9 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → V ∈ A
10 eqid ⊢ Base K = Base K
11 10 2 3 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ V ∈ A → P ∨ ˙ V ∈ Base K
12 4 8 9 11 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∨ ˙ V ∈ Base K
13 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → W ∈ A
14 10 3 atbase ⊢ W ∈ A → W ∈ Base K
15 13 14 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → W ∈ Base K
16 10 2 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ V ∈ Base K ∧ W ∈ Base K → P ∨ ˙ V ∨ ˙ W ∈ Base K
17 7 12 15 16 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∨ ˙ V ∨ ˙ W ∈ Base K
18 simp3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W
19 10 1 2 3 hlexchb2 ⊢ K ∈ HL ∧ Q ∈ A ∧ U ∈ A ∧ P ∨ ˙ V ∨ ˙ W ∈ Base K ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ≤ ˙ U ∨ ˙ P ∨ ˙ V ∨ ˙ W ↔ Q ∨ ˙ P ∨ ˙ V ∨ ˙ W = U ∨ ˙ P ∨ ˙ V ∨ ˙ W
20 4 5 6 17 18 19 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ≤ ˙ U ∨ ˙ P ∨ ˙ V ∨ ˙ W ↔ Q ∨ ˙ P ∨ ˙ V ∨ ˙ W = U ∨ ˙ P ∨ ˙ V ∨ ˙ W
21 1 2 3 4atlem4b ⊢ K ∈ HL ∧ P ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A → P ∨ ˙ U ∨ ˙ V ∨ ˙ W = U ∨ ˙ P ∨ ˙ V ∨ ˙ W
22 4 8 6 9 13 21 syl32anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∨ ˙ U ∨ ˙ V ∨ ˙ W = U ∨ ˙ P ∨ ˙ V ∨ ˙ W
23 22 breq2d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ≤ ˙ P ∨ ˙ U ∨ ˙ V ∨ ˙ W ↔ Q ≤ ˙ U ∨ ˙ P ∨ ˙ V ∨ ˙ W
24 1 2 3 4atlem4b ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ V ∈ A ∧ W ∈ A → P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = Q ∨ ˙ P ∨ ˙ V ∨ ˙ W
25 4 8 5 9 13 24 syl32anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = Q ∨ ˙ P ∨ ˙ V ∨ ˙ W
26 25 22 eqeq12d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = P ∨ ˙ U ∨ ˙ V ∨ ˙ W ↔ Q ∨ ˙ P ∨ ˙ V ∨ ˙ W = U ∨ ˙ P ∨ ˙ V ∨ ˙ W
27 20 23 26 3bitr4d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ U ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ V ∨ ˙ W → Q ≤ ˙ P ∨ ˙ U ∨ ˙ V ∨ ˙ W ↔ P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = P ∨ ˙ U ∨ ˙ V ∨ ˙ W