Metamath Proof Explorer

Theorem atmod4i1

Description: Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012) (Revised by Mario Carneiro, 10-May-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 atmod4i1 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → X ∧ ˙ Y ∨ ˙ P = X ∨ ˙ P ∧ ˙ 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 ∧ P ≤ ˙ Y → K ∈ Lat
8 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → X ∈ B
9 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → Y ∈ B
10 1 4 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y ∈ B
11 7 8 9 10 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → X ∧ ˙ Y ∈ B
12 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → P ∈ A
13 1 5 atbase ⊢ P ∈ A → P ∈ B
14 12 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → P ∈ B
15 1 3 latjcom ⊢ K ∈ Lat ∧ X ∧ ˙ Y ∈ B ∧ P ∈ B → X ∧ ˙ Y ∨ ˙ P = P ∨ ˙ X ∧ ˙ Y
16 7 11 14 15 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → X ∧ ˙ Y ∨ ˙ P = P ∨ ˙ X ∧ ˙ Y
17 1 2 3 4 5 atmod1i1 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → P ∨ ˙ X ∧ ˙ Y = P ∨ ˙ X ∧ ˙ Y
18 1 3 latjcom ⊢ K ∈ Lat ∧ P ∈ B ∧ X ∈ B → P ∨ ˙ X = X ∨ ˙ P
19 7 14 8 18 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → P ∨ ˙ X = X ∨ ˙ P
20 19 oveq1d ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → P ∨ ˙ X ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
21 16 17 20 3eqtrd ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ P ≤ ˙ Y → X ∧ ˙ Y ∨ ˙ P = X ∨ ˙ P ∧ ˙ Y