Metamath Proof Explorer

Theorem atmod1i2

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-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 atmod1i2 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = 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 simpl ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
7 simpr2 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → X ∈ B
8 simpr1 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → P ∈ A
9 eqid ⊢ pmap ⁡ K = pmap ⁡ K
10 eqid ⊢ + 𝑃 ⁡ K = + 𝑃 ⁡ K
11 1 3 5 9 10 pmapjat1 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → pmap ⁡ K ⁡ X ∨ ˙ P = pmap ⁡ K ⁡ X + 𝑃 ⁡ K pmap ⁡ K ⁡ P
12 6 7 8 11 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → pmap ⁡ K ⁡ X ∨ ˙ P = pmap ⁡ K ⁡ X + 𝑃 ⁡ K pmap ⁡ K ⁡ P
13 1 5 atbase ⊢ P ∈ A → P ∈ B
14 8 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → P ∈ B
15 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
16 1 2 3 4 9 10 hlmod1i ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ pmap ⁡ K ⁡ X ∨ ˙ P = pmap ⁡ K ⁡ X + 𝑃 ⁡ K pmap ⁡ K ⁡ P → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
17 6 7 14 15 16 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ∧ pmap ⁡ K ⁡ X ∨ ˙ P = pmap ⁡ K ⁡ X + 𝑃 ⁡ K pmap ⁡ K ⁡ P → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
18 12 17 mpan2d ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
19 18 3impia ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y
20 19 eqcomd ⊢ K ∈ HL ∧ P ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ X ≤ ˙ Y → X ∨ ˙ P ∧ ˙ Y = X ∨ ˙ P ∧ ˙ Y