Metamath Proof Explorer

Theorem pexmidN

Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N . Lemma 3.3(2) in Holland95 p. 215, which we prove as a special case of osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmid.a 
|- A = ( Atoms ` K )
pexmid.p 
|- .+ = ( +P ` K )
pexmid.o 
|- ._|_ = ( _|_P ` K )
Assertion pexmidN 
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )

Proof

Step Hyp Ref Expression
1 pexmid.a 
 |-  A = ( Atoms ` K )
2 pexmid.p 
 |-  .+ = ( +P ` K )
3 pexmid.o 
 |-  ._|_ = ( _|_P ` K )
4 simpll 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> K e. HL )
5 simplr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> X C_ A )
6 1 3 polssatN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
7 6 adantr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` X ) C_ A )
8 1 2 3 poldmj1N 
 |-  ( ( K e. HL /\ X C_ A /\ ( ._|_ ` X ) C_ A ) -> ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) )
9 4 5 7 8 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) )
10 1 3 pnonsingN 
 |-  ( ( K e. HL /\ ( ._|_ ` X ) C_ A ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) = (/) )
11 4 7 10 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) = (/) )
12 9 11 eqtrd 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) = (/) )
13 12 fveq2d 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) ) = ( ._|_ ` (/) ) )
14 simpr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
15 eqid 
 |-  ( PSubCl ` K ) = ( PSubCl ` K )
16 1 3 15 ispsubclN 
 |-  ( K e. HL -> ( X e. ( PSubCl ` K ) <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
17 16 ad2antrr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X e. ( PSubCl ` K ) <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
18 5 14 17 mpbir2and 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> X e. ( PSubCl ` K ) )
19 1 3 15 polsubclN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. ( PSubCl ` K ) )
20 19 adantr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` X ) e. ( PSubCl ` K ) )
21 1 3 2polssN 
 |-  ( ( K e. HL /\ X C_ A ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
22 21 adantr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
23 2 3 15 osumclN 
 |-  ( ( ( K e. HL /\ X e. ( PSubCl ` K ) /\ ( ._|_ ` X ) e. ( PSubCl ` K ) ) /\ X C_ ( ._|_ ` ( ._|_ ` X ) ) ) -> ( X .+ ( ._|_ ` X ) ) e. ( PSubCl ` K ) )
24 4 18 20 22 23 syl31anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) e. ( PSubCl ` K ) )
25 3 15 psubcli2N 
 |-  ( ( K e. HL /\ ( X .+ ( ._|_ ` X ) ) e. ( PSubCl ` K ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) ) = ( X .+ ( ._|_ ` X ) ) )
26 4 24 25 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( ._|_ ` ( X .+ ( ._|_ ` X ) ) ) ) = ( X .+ ( ._|_ ` X ) ) )
27 1 3 pol0N 
 |-  ( K e. HL -> ( ._|_ ` (/) ) = A )
28 27 ad2antrr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` (/) ) = A )
29 13 26 28 3eqtr3d 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )