Metamath Proof Explorer

Theorem poml4N

Description: Orthomodular law for projective lattices. Lemma 3.3(1) in Holland95 p. 215. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses poml4.a ⊢A=Atoms⁡K
poml4.p ⊢⊥˙=⊥𝑃⁡K
Assertion poml4N ⊢K∈HL∧X⊆A∧Y⊆A→X⊆Y∧⊥˙⁡⊥˙⁡Y=Y→⊥˙⁡⊥˙⁡X∩Y∩Y=⊥˙⁡⊥˙⁡X

Proof

Step Hyp Ref Expression
1 poml4.a ⊢A=Atoms⁡K
2 poml4.p ⊢⊥˙=⊥𝑃⁡K
3 eqcom ⊢⊥˙⁡⊥˙⁡Y=Y↔Y=⊥˙⁡⊥˙⁡Y
4 eqid ⊢lub⁡K=lub⁡K
5 eqid ⊢pmap⁡K=pmap⁡K
6 4 1 5 2 2polvalN ⊢K∈HL∧Y⊆A→⊥˙⁡⊥˙⁡Y=pmap⁡K⁡lub⁡K⁡Y
7 6 3adant2 ⊢K∈HL∧X⊆A∧Y⊆A→⊥˙⁡⊥˙⁡Y=pmap⁡K⁡lub⁡K⁡Y
8 7 eqeq2d ⊢K∈HL∧X⊆A∧Y⊆A→Y=⊥˙⁡⊥˙⁡Y↔Y=pmap⁡K⁡lub⁡K⁡Y
9 8 biimpd ⊢K∈HL∧X⊆A∧Y⊆A→Y=⊥˙⁡⊥˙⁡Y→Y=pmap⁡K⁡lub⁡K⁡Y
10 3 9 syl5bi ⊢K∈HL∧X⊆A∧Y⊆A→⊥˙⁡⊥˙⁡Y=Y→Y=pmap⁡K⁡lub⁡K⁡Y
11 simpl1 ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈HL
12 hloml ⊢K∈HL→K∈OML
13 11 12 syl ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈OML
14 hlclat ⊢K∈HL→K∈CLat
15 11 14 syl ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈CLat
16 simpl2 ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→X⊆A
17 eqid ⊢BaseK=BaseK
18 17 1 atssbase ⊢A⊆BaseK
19 16 18 sstrdi ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→X⊆BaseK
20 17 4 clatlubcl ⊢K∈CLat∧X⊆BaseK→lub⁡K⁡X∈BaseK
21 15 19 20 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→lub⁡K⁡X∈BaseK
22 simpl3 ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→Y⊆A
23 22 18 sstrdi ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→Y⊆BaseK
24 17 4 clatlubcl ⊢K∈CLat∧Y⊆BaseK→lub⁡K⁡Y∈BaseK
25 15 23 24 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→lub⁡K⁡Y∈BaseK
26 13 21 25 3jca ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈OML∧lub⁡K⁡X∈BaseK∧lub⁡K⁡Y∈BaseK
27 simprl ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→X⊆Y
28 eqid ⊢≤K=≤K
29 17 28 4 lubss ⊢K∈CLat∧Y⊆BaseK∧X⊆Y→lub⁡K⁡X≤Klub⁡K⁡Y
30 15 23 27 29 syl3anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→lub⁡K⁡X≤Klub⁡K⁡Y
31 eqid ⊢meet⁡K=meet⁡K
32 eqid ⊢oc⁡K=oc⁡K
33 17 28 31 32 omllaw4 ⊢K∈OML∧lub⁡K⁡X∈BaseK∧lub⁡K⁡Y∈BaseK→lub⁡K⁡X≤Klub⁡K⁡Y→oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y=lub⁡K⁡X
34 26 30 33 sylc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y=lub⁡K⁡X
35 34 fveq2d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y=pmap⁡K⁡lub⁡K⁡X
36 4 32 1 5 2 polval2N ⊢K∈HL∧X⊆A→⊥˙⁡X=pmap⁡K⁡oc⁡K⁡lub⁡K⁡X
37 11 16 36 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡X=pmap⁡K⁡oc⁡K⁡lub⁡K⁡X
38 simprr ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→Y=pmap⁡K⁡lub⁡K⁡Y
39 37 38 ineq12d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡X∩Y=pmap⁡K⁡oc⁡K⁡lub⁡K⁡X∩pmap⁡K⁡lub⁡K⁡Y
40 hlop ⊢K∈HL→K∈OP
41 11 40 syl ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈OP
42 17 32 opoccl ⊢K∈OP∧lub⁡K⁡X∈BaseK→oc⁡K⁡lub⁡K⁡X∈BaseK
43 41 21 42 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→oc⁡K⁡lub⁡K⁡X∈BaseK
44 17 31 1 5 pmapmeet ⊢K∈HL∧oc⁡K⁡lub⁡K⁡X∈BaseK∧lub⁡K⁡Y∈BaseK→pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡lub⁡K⁡X∩pmap⁡K⁡lub⁡K⁡Y
45 11 43 25 44 syl3anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡lub⁡K⁡X∩pmap⁡K⁡lub⁡K⁡Y
46 39 45 eqtr4d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡X∩Y=pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y
47 46 fveq2d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y=⊥˙⁡pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y
48 11 hllatd ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→K∈Lat
49 17 31 latmcl ⊢K∈Lat∧oc⁡K⁡lub⁡K⁡X∈BaseK∧lub⁡K⁡Y∈BaseK→oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK
50 48 43 25 49 syl3anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK
51 17 32 5 2 polpmapN ⊢K∈HL∧oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK→⊥˙⁡pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y
52 11 50 51 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡pmap⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y
53 47 52 eqtrd ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y
54 53 38 ineq12d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y∩Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∩pmap⁡K⁡lub⁡K⁡Y
55 17 32 opoccl ⊢K∈OP∧oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK→oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK
56 41 50 55 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK
57 17 31 1 5 pmapmeet ⊢K∈HL∧oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∈BaseK∧lub⁡K⁡Y∈BaseK→pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∩pmap⁡K⁡lub⁡K⁡Y
58 11 56 25 57 syl3anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Y∩pmap⁡K⁡lub⁡K⁡Y
59 54 58 eqtr4d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y∩Y=pmap⁡K⁡oc⁡K⁡oc⁡K⁡lub⁡K⁡Xmeet⁡Klub⁡K⁡Ymeet⁡Klub⁡K⁡Y
60 4 1 5 2 2polvalN ⊢K∈HL∧X⊆A→⊥˙⁡⊥˙⁡X=pmap⁡K⁡lub⁡K⁡X
61 11 16 60 syl2anc ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X=pmap⁡K⁡lub⁡K⁡X
62 35 59 61 3eqtr4d ⊢K∈HL∧X⊆A∧Y⊆A∧X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y∩Y=⊥˙⁡⊥˙⁡X
63 62 ex ⊢K∈HL∧X⊆A∧Y⊆A→X⊆Y∧Y=pmap⁡K⁡lub⁡K⁡Y→⊥˙⁡⊥˙⁡X∩Y∩Y=⊥˙⁡⊥˙⁡X
64 10 63 sylan2d ⊢K∈HL∧X⊆A∧Y⊆A→X⊆Y∧⊥˙⁡⊥˙⁡Y=Y→⊥˙⁡⊥˙⁡X∩Y∩Y=⊥˙⁡⊥˙⁡X