# Metamath Proof Explorer

## Theorem poml6N

Description: Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses poml6.c ${⊢}{C}=\mathrm{PSubCl}\left({K}\right)$
poml6.p
Assertion poml6N

### Proof

Step Hyp Ref Expression
1 poml6.c ${⊢}{C}=\mathrm{PSubCl}\left({K}\right)$
2 poml6.p
3 simpl1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {K}\in \mathrm{HL}$
4 simpl2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {X}\in {C}$
5 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
6 5 1 psubclssatN ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {C}\right)\to {X}\subseteq \mathrm{Atoms}\left({K}\right)$
7 3 4 6 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {X}\subseteq \mathrm{Atoms}\left({K}\right)$
8 simpl3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {Y}\in {C}$
9 5 1 psubclssatN ${⊢}\left({K}\in \mathrm{HL}\wedge {Y}\in {C}\right)\to {Y}\subseteq \mathrm{Atoms}\left({K}\right)$
10 3 8 9 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {Y}\subseteq \mathrm{Atoms}\left({K}\right)$
11 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {C}\wedge {Y}\in {C}\right)\wedge {X}\subseteq {Y}\right)\to {X}\subseteq {Y}$
12 2 1 psubcli2N
13 3 8 12 syl2anc
14 5 2 poml4N
15 14 imp
16 3 7 10 11 13 15 syl32anc
17 2 1 psubcli2N
18 3 4 17 syl2anc
19 16 18 eqtrd