Metamath Proof Explorer


Theorem atmod2i1

Description: Version of modular law pmod2iN 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=BaseK
atmod.l ˙=K
atmod.j ˙=joinK
atmod.m ˙=meetK
atmod.a A=AtomsK
Assertion atmod2i1 KHLPAXBYBP˙XX˙Y˙P=X˙Y˙P

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 hllat KHLKLat
7 6 3ad2ant1 KHLPAXBYBP˙XKLat
8 simp22 KHLPAXBYBP˙XXB
9 simp23 KHLPAXBYBP˙XYB
10 1 4 latmcom KLatXBYBX˙Y=Y˙X
11 7 8 9 10 syl3anc KHLPAXBYBP˙XX˙Y=Y˙X
12 11 oveq2d KHLPAXBYBP˙XP˙X˙Y=P˙Y˙X
13 simp21 KHLPAXBYBP˙XPA
14 1 5 atbase PAPB
15 13 14 syl KHLPAXBYBP˙XPB
16 1 4 latmcl KLatXBYBX˙YB
17 7 8 9 16 syl3anc KHLPAXBYBP˙XX˙YB
18 1 3 latjcom KLatPBX˙YBP˙X˙Y=X˙Y˙P
19 7 15 17 18 syl3anc KHLPAXBYBP˙XP˙X˙Y=X˙Y˙P
20 1 3 latjcl KLatPBYBP˙YB
21 7 15 9 20 syl3anc KHLPAXBYBP˙XP˙YB
22 1 4 latmcom KLatP˙YBXBP˙Y˙X=X˙P˙Y
23 7 21 8 22 syl3anc KHLPAXBYBP˙XP˙Y˙X=X˙P˙Y
24 simp1 KHLPAXBYBP˙XKHL
25 simp3 KHLPAXBYBP˙XP˙X
26 1 2 3 4 5 atmod1i1 KHLPAYBXBP˙XP˙Y˙X=P˙Y˙X
27 24 13 9 8 25 26 syl131anc KHLPAXBYBP˙XP˙Y˙X=P˙Y˙X
28 1 3 latjcom KLatYBPBY˙P=P˙Y
29 7 9 15 28 syl3anc KHLPAXBYBP˙XY˙P=P˙Y
30 29 oveq2d KHLPAXBYBP˙XX˙Y˙P=X˙P˙Y
31 23 27 30 3eqtr4d KHLPAXBYBP˙XP˙Y˙X=X˙Y˙P
32 12 19 31 3eqtr3d KHLPAXBYBP˙XX˙Y˙P=X˙Y˙P