Metamath Proof Explorer


Theorem lhpmod2i2

Description: Modular law for hyperplanes analogous to atmod2i2 for atoms. (Contributed by NM, 9-Feb-2013)

Ref Expression
Hypotheses lhpmod.b B = Base K
lhpmod.l ˙ = K
lhpmod.j ˙ = join K
lhpmod.m ˙ = meet K
lhpmod.h H = LHyp K
Assertion lhpmod2i2 K HL W H X B Y B Y ˙ X X ˙ W ˙ Y = X ˙ W ˙ Y

Proof

Step Hyp Ref Expression
1 lhpmod.b B = Base K
2 lhpmod.l ˙ = K
3 lhpmod.j ˙ = join K
4 lhpmod.m ˙ = meet K
5 lhpmod.h H = LHyp K
6 simp1l K HL W H X B Y B Y ˙ X K HL
7 simp1r K HL W H X B Y B Y ˙ X W H
8 eqid oc K = oc K
9 eqid Atoms K = Atoms K
10 8 9 5 lhpocat K HL W H oc K W Atoms K
11 6 7 10 syl2anc K HL W H X B Y B Y ˙ X oc K W Atoms K
12 hlop K HL K OP
13 6 12 syl K HL W H X B Y B Y ˙ X K OP
14 simp2l K HL W H X B Y B Y ˙ X X B
15 1 8 opoccl K OP X B oc K X B
16 13 14 15 syl2anc K HL W H X B Y B Y ˙ X oc K X B
17 simp2r K HL W H X B Y B Y ˙ X Y B
18 1 8 opoccl K OP Y B oc K Y B
19 13 17 18 syl2anc K HL W H X B Y B Y ˙ X oc K Y B
20 simp3 K HL W H X B Y B Y ˙ X Y ˙ X
21 1 2 8 oplecon3b K OP Y B X B Y ˙ X oc K X ˙ oc K Y
22 13 17 14 21 syl3anc K HL W H X B Y B Y ˙ X Y ˙ X oc K X ˙ oc K Y
23 20 22 mpbid K HL W H X B Y B Y ˙ X oc K X ˙ oc K Y
24 1 2 3 4 9 atmod1i2 K HL oc K W Atoms K oc K X B oc K Y B oc K X ˙ oc K Y oc K X ˙ oc K W ˙ oc K Y = oc K X ˙ oc K W ˙ oc K Y
25 6 11 16 19 23 24 syl131anc K HL W H X B Y B Y ˙ X oc K X ˙ oc K W ˙ oc K Y = oc K X ˙ oc K W ˙ oc K Y
26 6 hllatd K HL W H X B Y B Y ˙ X K Lat
27 1 5 lhpbase W H W B
28 7 27 syl K HL W H X B Y B Y ˙ X W B
29 1 4 latmcl K Lat X B W B X ˙ W B
30 26 14 28 29 syl3anc K HL W H X B Y B Y ˙ X X ˙ W B
31 1 3 latjcl K Lat X ˙ W B Y B X ˙ W ˙ Y B
32 26 30 17 31 syl3anc K HL W H X B Y B Y ˙ X X ˙ W ˙ Y B
33 1 3 latjcl K Lat W B Y B W ˙ Y B
34 26 28 17 33 syl3anc K HL W H X B Y B Y ˙ X W ˙ Y B
35 1 4 latmcl K Lat X B W ˙ Y B X ˙ W ˙ Y B
36 26 14 34 35 syl3anc K HL W H X B Y B Y ˙ X X ˙ W ˙ Y B
37 1 8 opcon3b K OP X ˙ W ˙ Y B X ˙ W ˙ Y B X ˙ W ˙ Y = X ˙ W ˙ Y oc K X ˙ W ˙ Y = oc K X ˙ W ˙ Y
38 13 32 36 37 syl3anc K HL W H X B Y B Y ˙ X X ˙ W ˙ Y = X ˙ W ˙ Y oc K X ˙ W ˙ Y = oc K X ˙ W ˙ Y
39 hlol K HL K OL
40 6 39 syl K HL W H X B Y B Y ˙ X K OL
41 1 3 4 8 oldmm1 K OL X B W ˙ Y B oc K X ˙ W ˙ Y = oc K X ˙ oc K W ˙ Y
42 40 14 34 41 syl3anc K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ Y = oc K X ˙ oc K W ˙ Y
43 1 3 4 8 oldmj1 K OL W B Y B oc K W ˙ Y = oc K W ˙ oc K Y
44 40 28 17 43 syl3anc K HL W H X B Y B Y ˙ X oc K W ˙ Y = oc K W ˙ oc K Y
45 44 oveq2d K HL W H X B Y B Y ˙ X oc K X ˙ oc K W ˙ Y = oc K X ˙ oc K W ˙ oc K Y
46 42 45 eqtrd K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ Y = oc K X ˙ oc K W ˙ oc K Y
47 1 3 4 8 oldmj1 K OL X ˙ W B Y B oc K X ˙ W ˙ Y = oc K X ˙ W ˙ oc K Y
48 40 30 17 47 syl3anc K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ Y = oc K X ˙ W ˙ oc K Y
49 1 3 4 8 oldmm1 K OL X B W B oc K X ˙ W = oc K X ˙ oc K W
50 40 14 28 49 syl3anc K HL W H X B Y B Y ˙ X oc K X ˙ W = oc K X ˙ oc K W
51 50 oveq1d K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ oc K Y = oc K X ˙ oc K W ˙ oc K Y
52 48 51 eqtrd K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ Y = oc K X ˙ oc K W ˙ oc K Y
53 46 52 eqeq12d K HL W H X B Y B Y ˙ X oc K X ˙ W ˙ Y = oc K X ˙ W ˙ Y oc K X ˙ oc K W ˙ oc K Y = oc K X ˙ oc K W ˙ oc K Y
54 38 53 bitrd K HL W H X B Y B Y ˙ X X ˙ W ˙ Y = X ˙ W ˙ Y oc K X ˙ oc K W ˙ oc K Y = oc K X ˙ oc K W ˙ oc K Y
55 25 54 mpbird K HL W H X B Y B Y ˙ X X ˙ W ˙ Y = X ˙ W ˙ Y