# Metamath Proof Explorer

## Theorem llnmod2i2

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 llnmod2i2

### 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 simp11
7 6 hllatd
8 simp13
9 simp2l
10 simp2r
11 1 3 5 hlatjcl
12 6 9 10 11 syl3anc
13 simp12
14 1 4 latmcl
15 7 12 13 14 syl3anc
16 1 3 latjcom
17 7 8 15 16 syl3anc
18 1 3 latjcl
19 7 8 12 18 syl3anc
20 1 4 latmcom
21 7 13 19 20 syl3anc
22 1 3 latjcom
23 7 12 8 22 syl3anc
24 23 oveq2d
25 simp3
26 1 2 3 4 5 llnmod1i2
27 6 8 13 9 10 25 26 syl321anc
28 21 24 27 3eqtr4d
29 1 4 latmcom
30 7 13 12 29 syl3anc
31 30 oveq1d
32 17 28 31 3eqtr4rd