Metamath Proof Explorer


Theorem pl42N

Description: Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in MegPav2000 p. 2366). (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42.b B = Base K
pl42.l ˙ = K
pl42.j ˙ = join K
pl42.m ˙ = meet K
pl42.o ˙ = oc K
Assertion pl42N K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z ˙ W ˙ V ˙ X ˙ Y ˙ X ˙ W ˙ Y ˙ V

Proof

Step Hyp Ref Expression
1 pl42.b B = Base K
2 pl42.l ˙ = K
3 pl42.j ˙ = join K
4 pl42.m ˙ = meet K
5 pl42.o ˙ = oc K
6 eqid pmap K = pmap K
7 eqid + 𝑃 K = + 𝑃 K
8 1 2 3 4 5 6 7 pl42lem4N K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W pmap K X ˙ Y ˙ Z ˙ W ˙ V pmap K X ˙ Y ˙ X ˙ W ˙ Y ˙ V
9 simpl1 K HL X B Y B Z B W B V B K HL
10 9 hllatd K HL X B Y B Z B W B V B K Lat
11 simpl2 K HL X B Y B Z B W B V B X B
12 simpl3 K HL X B Y B Z B W B V B Y B
13 1 3 latjcl K Lat X B Y B X ˙ Y B
14 10 11 12 13 syl3anc K HL X B Y B Z B W B V B X ˙ Y B
15 simpr1 K HL X B Y B Z B W B V B Z B
16 1 4 latmcl K Lat X ˙ Y B Z B X ˙ Y ˙ Z B
17 10 14 15 16 syl3anc K HL X B Y B Z B W B V B X ˙ Y ˙ Z B
18 simpr2 K HL X B Y B Z B W B V B W B
19 1 3 latjcl K Lat X ˙ Y ˙ Z B W B X ˙ Y ˙ Z ˙ W B
20 10 17 18 19 syl3anc K HL X B Y B Z B W B V B X ˙ Y ˙ Z ˙ W B
21 simpr3 K HL X B Y B Z B W B V B V B
22 1 4 latmcl K Lat X ˙ Y ˙ Z ˙ W B V B X ˙ Y ˙ Z ˙ W ˙ V B
23 10 20 21 22 syl3anc K HL X B Y B Z B W B V B X ˙ Y ˙ Z ˙ W ˙ V B
24 1 3 latjcl K Lat X B W B X ˙ W B
25 10 11 18 24 syl3anc K HL X B Y B Z B W B V B X ˙ W B
26 1 3 latjcl K Lat Y B V B Y ˙ V B
27 10 12 21 26 syl3anc K HL X B Y B Z B W B V B Y ˙ V B
28 1 4 latmcl K Lat X ˙ W B Y ˙ V B X ˙ W ˙ Y ˙ V B
29 10 25 27 28 syl3anc K HL X B Y B Z B W B V B X ˙ W ˙ Y ˙ V B
30 1 3 latjcl K Lat X ˙ Y B X ˙ W ˙ Y ˙ V B X ˙ Y ˙ X ˙ W ˙ Y ˙ V B
31 10 14 29 30 syl3anc K HL X B Y B Z B W B V B X ˙ Y ˙ X ˙ W ˙ Y ˙ V B
32 1 2 6 pmaple K HL X ˙ Y ˙ Z ˙ W ˙ V B X ˙ Y ˙ X ˙ W ˙ Y ˙ V B X ˙ Y ˙ Z ˙ W ˙ V ˙ X ˙ Y ˙ X ˙ W ˙ Y ˙ V pmap K X ˙ Y ˙ Z ˙ W ˙ V pmap K X ˙ Y ˙ X ˙ W ˙ Y ˙ V
33 9 23 31 32 syl3anc K HL X B Y B Z B W B V B X ˙ Y ˙ Z ˙ W ˙ V ˙ X ˙ Y ˙ X ˙ W ˙ Y ˙ V pmap K X ˙ Y ˙ Z ˙ W ˙ V pmap K X ˙ Y ˙ X ˙ W ˙ Y ˙ V
34 8 33 sylibrd K HL X B Y B Z B W B V B X ˙ ˙ Y Z ˙ ˙ W X ˙ Y ˙ Z ˙ W ˙ V ˙ X ˙ Y ˙ X ˙ W ˙ Y ˙ V