Metamath Proof Explorer

Theorem dochpolN

Description: The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dochpol.h 
|- H = ( LHyp ` K )
dochpol.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochpol.u 
|- U = ( ( DVecH ` K ) ` W )
dochpol.p 
|- P = ( LPol ` U )
dochpol.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dochpolN 
|- ( ph -> ._|_ e. P )

Proof

Step Hyp Ref Expression
1 dochpol.h 
 |-  H = ( LHyp ` K )
2 dochpol.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochpol.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochpol.p 
 |-  P = ( LPol ` U )
5 dochpol.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 eqid 
 |-  ( Base ` U ) = ( Base ` U )
7 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
8 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
9 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
10 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
11 3 fvexi 
 |-  U e. _V
12 11 a1i 
 |-  ( ph -> U e. _V )
13 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
14 1 13 3 6 2 5 dochfN 
 |-  ( ph -> ._|_ : ~P ( Base ` U ) --> ran ( ( DIsoH ` K ) ` W ) )
15 1 3 13 7 dihsslss 
 |-  ( ( K e. HL /\ W e. H ) -> ran ( ( DIsoH ` K ) ` W ) C_ ( LSubSp ` U ) )
16 5 15 syl 
 |-  ( ph -> ran ( ( DIsoH ` K ) ` W ) C_ ( LSubSp ` U ) )
17 14 16 fssd 
 |-  ( ph -> ._|_ : ~P ( Base ` U ) --> ( LSubSp ` U ) )
18 1 3 2 6 8 doch1 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` ( Base ` U ) ) = { ( 0g ` U ) } )
19 5 18 syl 
 |-  ( ph -> ( ._|_ ` ( Base ` U ) ) = { ( 0g ` U ) } )
20 5 adantr 
 |-  ( ( ph /\ ( x C_ ( Base ` U ) /\ y C_ ( Base ` U ) /\ x C_ y ) ) -> ( K e. HL /\ W e. H ) )
21 simpr2 
 |-  ( ( ph /\ ( x C_ ( Base ` U ) /\ y C_ ( Base ` U ) /\ x C_ y ) ) -> y C_ ( Base ` U ) )
22 simpr3 
 |-  ( ( ph /\ ( x C_ ( Base ` U ) /\ y C_ ( Base ` U ) /\ x C_ y ) ) -> x C_ y )
23 1 3 6 2 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y C_ ( Base ` U ) /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
24 20 21 22 23 syl3anc 
 |-  ( ( ph /\ ( x C_ ( Base ` U ) /\ y C_ ( Base ` U ) /\ x C_ y ) ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) )
25 5 adantr 
 |-  ( ( ph /\ x e. ( LSAtoms ` U ) ) -> ( K e. HL /\ W e. H ) )
26 simpr 
 |-  ( ( ph /\ x e. ( LSAtoms ` U ) ) -> x e. ( LSAtoms ` U ) )
27 1 3 2 9 10 25 26 dochsatshp 
 |-  ( ( ph /\ x e. ( LSAtoms ` U ) ) -> ( ._|_ ` x ) e. ( LSHyp ` U ) )
28 1 3 13 9 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ( LSAtoms ` U ) ) -> x e. ran ( ( DIsoH ` K ) ` W ) )
29 25 26 28 syl2anc 
 |-  ( ( ph /\ x e. ( LSAtoms ` U ) ) -> x e. ran ( ( DIsoH ` K ) ` W ) )
30 1 13 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )
31 25 29 30 syl2anc 
 |-  ( ( ph /\ x e. ( LSAtoms ` U ) ) -> ( ._|_ ` ( ._|_ ` x ) ) = x )
32 6 7 8 9 10 4 12 17 19 24 27 31 islpoldN 
 |-  ( ph -> ._|_ e. P )