Metamath Proof Explorer


Theorem atmod3i1

Description: Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-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 atmod3i1 KHLPAXBYBP˙XP˙X˙Y=X˙P˙Y

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 simp1 KHLPAXBYBP˙XKHL
7 simp21 KHLPAXBYBP˙XPA
8 simp23 KHLPAXBYBP˙XYB
9 simp22 KHLPAXBYBP˙XXB
10 simp3 KHLPAXBYBP˙XP˙X
11 1 2 3 4 5 atmod1i1 KHLPAYBXBP˙XP˙Y˙X=P˙Y˙X
12 6 7 8 9 10 11 syl131anc KHLPAXBYBP˙XP˙Y˙X=P˙Y˙X
13 hllat KHLKLat
14 13 3ad2ant1 KHLPAXBYBP˙XKLat
15 1 4 latmcom KLatXBYBX˙Y=Y˙X
16 14 9 8 15 syl3anc KHLPAXBYBP˙XX˙Y=Y˙X
17 16 oveq2d KHLPAXBYBP˙XP˙X˙Y=P˙Y˙X
18 1 5 atbase PAPB
19 7 18 syl KHLPAXBYBP˙XPB
20 1 3 latjcl KLatPBYBP˙YB
21 14 19 8 20 syl3anc KHLPAXBYBP˙XP˙YB
22 1 4 latmcom KLatXBP˙YBX˙P˙Y=P˙Y˙X
23 14 9 21 22 syl3anc KHLPAXBYBP˙XX˙P˙Y=P˙Y˙X
24 12 17 23 3eqtr4d KHLPAXBYBP˙XP˙X˙Y=X˙P˙Y