# 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}=\mathrm{Atoms}\left({K}\right)$
poml4.p
Assertion poml4N

### Proof

Step Hyp Ref Expression
1 poml4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2 poml4.p
3 eqcom
4 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\left({K}\right)$
5 eqid ${⊢}\mathrm{pmap}\left({K}\right)=\mathrm{pmap}\left({K}\right)$
6 4 1 5 2 2polvalN
8 7 eqeq2d
9 8 biimpd
10 3 9 syl5bi
11 simpl1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {K}\in \mathrm{HL}$
12 hloml ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OML}$
13 11 12 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {K}\in \mathrm{OML}$
14 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
15 11 14 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {K}\in \mathrm{CLat}$
16 simpl2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {X}\subseteq {A}$
17 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
18 17 1 atssbase ${⊢}{A}\subseteq {\mathrm{Base}}_{{K}}$
19 16 18 sstrdi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {X}\subseteq {\mathrm{Base}}_{{K}}$
20 17 4 clatlubcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {X}\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{lub}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}$
21 15 19 20 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{lub}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}$
22 simpl3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {Y}\subseteq {A}$
23 22 18 sstrdi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {Y}\subseteq {\mathrm{Base}}_{{K}}$
24 17 4 clatlubcl ${⊢}\left({K}\in \mathrm{CLat}\wedge {Y}\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}$
25 15 23 24 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}$
26 13 21 25 3jca ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \left({K}\in \mathrm{OML}\wedge \mathrm{lub}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)$
27 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {X}\subseteq {Y}$
28 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
29 17 28 4 lubss ${⊢}\left({K}\in \mathrm{CLat}\wedge {Y}\subseteq {\mathrm{Base}}_{{K}}\wedge {X}\subseteq {Y}\right)\to \mathrm{lub}\left({K}\right)\left({X}\right){\le }_{{K}}\mathrm{lub}\left({K}\right)\left({Y}\right)$
30 15 23 27 29 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{lub}\left({K}\right)\left({X}\right){\le }_{{K}}\mathrm{lub}\left({K}\right)\left({Y}\right)$
31 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
32 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
33 17 28 31 32 omllaw4 ${⊢}\left({K}\in \mathrm{OML}\wedge \mathrm{lub}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)\to \left(\mathrm{lub}\left({K}\right)\left({X}\right){\le }_{{K}}\mathrm{lub}\left({K}\right)\left({Y}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)=\mathrm{lub}\left({K}\right)\left({X}\right)\right)$
34 26 30 33 sylc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)=\mathrm{lub}\left({K}\right)\left({X}\right)$
35 34 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)$
36 4 32 1 5 2 polval2N
37 11 16 36 syl2anc
38 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)$
39 37 38 ineq12d
40 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
41 11 40 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {K}\in \mathrm{OP}$
42 17 32 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge \mathrm{lub}\left({K}\right)\left({X}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
43 41 21 42 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
44 17 31 1 5 pmapmeet ${⊢}\left({K}\in \mathrm{HL}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)=\mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\right)\cap \mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)$
45 11 43 25 44 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)=\mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\right)\cap \mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)$
46 39 45 eqtr4d
47 46 fveq2d
48 11 hllatd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to {K}\in \mathrm{Lat}$
49 17 31 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}$
50 48 43 25 49 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}$
51 17 32 5 2 polpmapN
52 11 50 51 syl2anc
53 47 52 eqtrd
54 53 38 ineq12d
55 17 32 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\in {\mathrm{Base}}_{{K}}$
56 41 50 55 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\in {\mathrm{Base}}_{{K}}$
57 17 31 1 5 pmapmeet ${⊢}\left({K}\in \mathrm{HL}\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\in {\mathrm{Base}}_{{K}}\wedge \mathrm{lub}\left({K}\right)\left({Y}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)=\mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\cap \mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)$
58 11 56 25 57 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge \left({X}\subseteq {Y}\wedge {Y}=\mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\right)\to \mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)=\mathrm{pmap}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({X}\right)\right)\mathrm{meet}\left({K}\right)\mathrm{lub}\left({K}\right)\left({Y}\right)\right)\right)\cap \mathrm{pmap}\left({K}\right)\left(\mathrm{lub}\left({K}\right)\left({Y}\right)\right)$
59 54 58 eqtr4d
60 4 1 5 2 2polvalN
61 11 16 60 syl2anc
62 35 59 61 3eqtr4d
63 62 ex
64 10 63 sylan2d