Metamath Proof Explorer

Theorem atmod4i2

Description: Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012) (Revised by Mario Carneiro, 10-Mar-2013)

Ref Expression
Hypotheses atmod.b ⊢ B = Base K
atmod.l ⊢ ≤ ˙ = ≤ K
atmod.j ⊢ ∨ ˙ = join ⁡ K
atmod.m ⊢ ∧ ˙ = meet ⁡ K
atmod.a ⊢ A = Atoms ⁡ K
Assertion atmod4i2 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∧ ˙ Y ∨ ˙ X = P ∨ ˙ X ∧ ˙ Y

Proof

Step Hyp Ref Expression
1 atmod.b ⊢ B = Base K
2 atmod.l ⊢ ≤ ˙ = ≤ K
3 atmod.j ⊢ ∨ ˙ = join ⁡ K
4 atmod.m ⊢ ∧ ˙ = meet ⁡ K
5 atmod.a ⊢ A = Atoms ⁡ K
6 hllat ⊢ K ∈ HL → K ∈ Lat
7 6 3ad2ant1 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → K ∈ Lat
8 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∈ A
9 1 5 atbase ⊢ P ∈ A → P ∈ B
10 8 9 syl ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∈ B
11 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → Y ∈ B
12 1 4 latmcl ⊢ K ∈ Lat ∧ P ∈ B ∧ Y ∈ B → P ∧ ˙ Y ∈ B
13 7 10 11 12 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∧ ˙ Y ∈ B
14 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∈ B
15 1 3 latjcom ⊢ K ∈ Lat ∧ P ∧ ˙ Y ∈ B ∧ X ∈ B → P ∧ ˙ Y ∨ ˙ X = X ∨ ˙ P ∧ ˙ Y
16 7 13 14 15 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∧ ˙ Y ∨ ˙ X = X ∨ ˙ P ∧ ˙ Y
17 1 2 3 4 5 atmod1i2 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
18 1 3 latjcom ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∈ B → X ∨ ˙ P = P ∨ ˙ X
19 7 14 10 18 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P = P ∨ ˙ X
20 19 oveq1d ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = P ∨ ˙ X ∧ ˙ Y
21 16 17 20 3eqtrd ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → P ∧ ˙ Y ∨ ˙ X = P ∨ ˙ X ∧ ˙ Y