# Metamath Proof Explorer

## Theorem llnmod1i2

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join P .\/ Q ). (Contributed by NM, 16-Sep-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 llnmod1i2

### 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 simpl1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{HL}$
7 simpl2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {X}\in {B}$
8 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {P}\in {A}$
9 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Q}\in {A}$
10 eqid ${⊢}\mathrm{pmap}\left({K}\right)=\mathrm{pmap}\left({K}\right)$
11 eqid ${⊢}{+}_{𝑃}\left({K}\right)={+}_{𝑃}\left({K}\right)$
12 1 3 5 10 11 pmapjlln1
13 6 7 8 9 12 syl13anc
14 6 hllatd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {K}\in \mathrm{Lat}$
15 1 5 atbase ${⊢}{P}\in {A}\to {P}\in {B}$
16 8 15 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {P}\in {B}$
17 1 5 atbase ${⊢}{Q}\in {A}\to {Q}\in {B}$
18 9 17 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Q}\in {B}$
19 1 3 latjcl
20 14 16 18 19 syl3anc
21 simpl3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\right)\right)\to {Y}\in {B}$
22 1 2 3 4 10 11 hlmod1i
23 6 7 20 21 22 syl13anc
24 13 23 mpan2d
25 24 3impia
26 25 eqcomd