Metamath Proof Explorer

Theorem 4atlem10a

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

Ref Expression
Hypotheses 4at.l ⊢ ≤ ˙ = ≤ K
4at.j ⊢ ∨ ˙ = join ⁡ K
4at.a ⊢ A = Atoms ⁡ K
Assertion 4atlem10a ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ≤ ˙ P ∨ ˙ Q ∨ ˙ V ∨ ˙ W ↔ P ∨ ˙ Q ∨ ˙ R ∨ ˙ W = P ∨ ˙ Q ∨ ˙ 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 ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → K ∈ HL
5 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ∈ A
6 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → V ∈ A
7 4 hllatd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → K ∈ Lat
8 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → K ∈ HL ∧ P ∈ A ∧ Q ∈ A
9 eqid ⊢ Base K = Base K
10 9 2 3 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
11 8 10 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → P ∨ ˙ Q ∈ Base K
12 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → W ∈ A
13 9 3 atbase ⊢ W ∈ A → W ∈ Base K
14 12 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → W ∈ Base K
15 9 2 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → P ∨ ˙ Q ∨ ˙ W ∈ Base K
16 7 11 14 15 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → P ∨ ˙ Q ∨ ˙ W ∈ Base K
17 simp3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W
18 9 1 2 3 hlexchb2 ⊢ K ∈ HL ∧ R ∈ A ∧ V ∈ A ∧ P ∨ ˙ Q ∨ ˙ W ∈ Base K ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ≤ ˙ V ∨ ˙ P ∨ ˙ Q ∨ ˙ W ↔ R ∨ ˙ P ∨ ˙ Q ∨ ˙ W = V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
19 4 5 6 16 17 18 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ≤ ˙ V ∨ ˙ P ∨ ˙ Q ∨ ˙ W ↔ R ∨ ˙ P ∨ ˙ Q ∨ ˙ W = V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
20 1 2 3 4atlem4c ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ V ∈ A ∧ W ∈ A → P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
21 8 6 12 20 syl12anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → P ∨ ˙ Q ∨ ˙ V ∨ ˙ W = V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
22 21 breq2d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ≤ ˙ P ∨ ˙ Q ∨ ˙ V ∨ ˙ W ↔ R ≤ ˙ V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
23 1 2 3 4atlem4c ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ W ∈ A → P ∨ ˙ Q ∨ ˙ R ∨ ˙ W = R ∨ ˙ P ∨ ˙ Q ∨ ˙ W
24 8 5 12 23 syl12anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → P ∨ ˙ Q ∨ ˙ R ∨ ˙ W = R ∨ ˙ P ∨ ˙ Q ∨ ˙ W
25 24 21 eqeq12d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → P ∨ ˙ Q ∨ ˙ R ∨ ˙ W = P ∨ ˙ Q ∨ ˙ V ∨ ˙ W ↔ R ∨ ˙ P ∨ ˙ Q ∨ ˙ W = V ∨ ˙ P ∨ ˙ Q ∨ ˙ W
26 19 22 25 3bitr4d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ V ∈ A ∧ W ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q ∨ ˙ W → R ≤ ˙ P ∨ ˙ Q ∨ ˙ V ∨ ˙ W ↔ P ∨ ˙ Q ∨ ˙ R ∨ ˙ W = P ∨ ˙ Q ∨ ˙ V ∨ ˙ W