# 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}={\mathrm{Base}}_{{K}}$
atmod.l
atmod.j
atmod.m
atmod.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion atmod1i2

### Proof

Step Hyp Ref Expression
1 atmod.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 atmod.l
3 atmod.j
4 atmod.m
5 atmod.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 simpl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {K}\in \mathrm{HL}$
7 simpr2 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
8 simpr1 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {P}\in {A}$
9 eqid ${⊢}\mathrm{pmap}\left({K}\right)=\mathrm{pmap}\left({K}\right)$
10 eqid ${⊢}{+}_{𝑃}\left({K}\right)={+}_{𝑃}\left({K}\right)$
11 1 3 5 9 10 pmapjat1
12 6 7 8 11 syl3anc
13 1 5 atbase ${⊢}{P}\in {A}\to {P}\in {B}$
14 8 13 syl ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {P}\in {B}$
15 simpr3 ${⊢}\left({K}\in \mathrm{HL}\wedge \left({P}\in {A}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
16 1 2 3 4 9 10 hlmod1i
17 6 7 14 15 16 syl13anc
18 12 17 mpan2d
19 18 3impia
20 19 eqcomd