Metamath Proof Explorer


Theorem atmod1i1m

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012) (Revised by Mario Carneiro, 10-May-2013)

Ref Expression
Hypotheses atmod.b B=BaseK
atmod.l ˙=K
atmod.j ˙=joinK
atmod.m ˙=meetK
atmod.a A=AtomsK
Assertion atmod1i1m KHLPAXBYBZBX˙P˙ZX˙P˙Y˙Z=X˙P˙Y˙Z

Proof

Step Hyp Ref Expression
1 atmod.b B=BaseK
2 atmod.l ˙=K
3 atmod.j ˙=joinK
4 atmod.m ˙=meetK
5 atmod.a A=AtomsK
6 simpl1l KHLPAXBYBZBX˙P˙ZX˙PAKHL
7 simpr KHLPAXBYBZBX˙P˙ZX˙PAX˙PA
8 simpl22 KHLPAXBYBZBX˙P˙ZX˙PAYB
9 simpl23 KHLPAXBYBZBX˙P˙ZX˙PAZB
10 simpl3 KHLPAXBYBZBX˙P˙ZX˙PAX˙P˙Z
11 1 2 3 4 5 atmod1i1 KHLX˙PAYBZBX˙P˙ZX˙P˙Y˙Z=X˙P˙Y˙Z
12 6 7 8 9 10 11 syl131anc KHLPAXBYBZBX˙P˙ZX˙PAX˙P˙Y˙Z=X˙P˙Y˙Z
13 simp1l KHLPAXBYBZBX˙P˙ZKHL
14 hlol KHLKOL
15 13 14 syl KHLPAXBYBZBX˙P˙ZKOL
16 15 adantr KHLPAXBYBZBX˙P˙ZX˙P=0.KKOL
17 13 hllatd KHLPAXBYBZBX˙P˙ZKLat
18 17 adantr KHLPAXBYBZBX˙P˙ZX˙P=0.KKLat
19 simpl22 KHLPAXBYBZBX˙P˙ZX˙P=0.KYB
20 simpl23 KHLPAXBYBZBX˙P˙ZX˙P=0.KZB
21 1 4 latmcl KLatYBZBY˙ZB
22 18 19 20 21 syl3anc KHLPAXBYBZBX˙P˙ZX˙P=0.KY˙ZB
23 eqid 0.K=0.K
24 1 3 23 olj02 KOLY˙ZB0.K˙Y˙Z=Y˙Z
25 16 22 24 syl2anc KHLPAXBYBZBX˙P˙ZX˙P=0.K0.K˙Y˙Z=Y˙Z
26 oveq1 X˙P=0.KX˙P˙Y˙Z=0.K˙Y˙Z
27 26 adantl KHLPAXBYBZBX˙P˙ZX˙P=0.KX˙P˙Y˙Z=0.K˙Y˙Z
28 oveq1 X˙P=0.KX˙P˙Y=0.K˙Y
29 28 adantl KHLPAXBYBZBX˙P˙ZX˙P=0.KX˙P˙Y=0.K˙Y
30 1 3 23 olj02 KOLYB0.K˙Y=Y
31 16 19 30 syl2anc KHLPAXBYBZBX˙P˙ZX˙P=0.K0.K˙Y=Y
32 29 31 eqtrd KHLPAXBYBZBX˙P˙ZX˙P=0.KX˙P˙Y=Y
33 32 oveq1d KHLPAXBYBZBX˙P˙ZX˙P=0.KX˙P˙Y˙Z=Y˙Z
34 25 27 33 3eqtr4d KHLPAXBYBZBX˙P˙ZX˙P=0.KX˙P˙Y˙Z=X˙P˙Y˙Z
35 simp21 KHLPAXBYBZBX˙P˙ZXB
36 simp1r KHLPAXBYBZBX˙P˙ZPA
37 1 4 23 5 meetat2 KOLXBPAX˙PAX˙P=0.K
38 15 35 36 37 syl3anc KHLPAXBYBZBX˙P˙ZX˙PAX˙P=0.K
39 12 34 38 mpjaodan KHLPAXBYBZBX˙P˙ZX˙P˙Y˙Z=X˙P˙Y˙Z