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 = ( PSubCl ` K )
poml6.p 
|- ._|_ = ( _|_P ` K )
Assertion poml6N 
|- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X )

Proof

Step Hyp Ref Expression
1 poml6.c 
 |-  C = ( PSubCl ` K )
2 poml6.p 
 |-  ._|_ = ( _|_P ` K )
3 simpl1 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> K e. HL )
4 simpl2 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> X e. C )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 5 1 psubclssatN 
 |-  ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
7 3 4 6 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> X C_ ( Atoms ` K ) )
8 simpl3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> Y e. C )
9 5 1 psubclssatN 
 |-  ( ( K e. HL /\ Y e. C ) -> Y C_ ( Atoms ` K ) )
10 3 8 9 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> Y C_ ( Atoms ` K ) )
11 simpr 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> X C_ Y )
12 2 1 psubcli2N 
 |-  ( ( K e. HL /\ Y e. C ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
13 3 8 12 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
14 5 2 poml4N 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( ( X C_ Y /\ ( ._|_ ` ( ._|_ ` Y ) ) = Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) ) )
15 14 imp 
 |-  ( ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) /\ ( X C_ Y /\ ( ._|_ ` ( ._|_ ` Y ) ) = Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) )
16 3 7 10 11 13 15 syl32anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) )
17 2 1 psubcli2N 
 |-  ( ( K e. HL /\ X e. C ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
18 3 4 17 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
19 16 18 eqtrd 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X )