Metamath Proof Explorer

Theorem docavalN

Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses docaval.j 
|- .\/ = ( join ` K )
docaval.m 
|- ./\ = ( meet ` K )
docaval.o 
|- ._|_ = ( oc ` K )
docaval.h 
|- H = ( LHyp ` K )
docaval.t 
|- T = ( ( LTrn ` K ) ` W )
docaval.i 
|- I = ( ( DIsoA ` K ) ` W )
docaval.n 
|- N = ( ( ocA ` K ) ` W )
Assertion docavalN 
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( N ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )

Proof

Step Hyp Ref Expression
1 docaval.j 
 |-  .\/ = ( join ` K )
2 docaval.m 
 |-  ./\ = ( meet ` K )
3 docaval.o 
 |-  ._|_ = ( oc ` K )
4 docaval.h 
 |-  H = ( LHyp ` K )
5 docaval.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 docaval.i 
 |-  I = ( ( DIsoA ` K ) ` W )
7 docaval.n 
 |-  N = ( ( ocA ` K ) ` W )
8 1 2 3 4 5 6 7 docafvalN 
 |-  ( ( K e. HL /\ W e. H ) -> N = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
9 8 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> N = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
10 9 fveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( N ` X ) = ( ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) ` X ) )
11 5 fvexi 
 |-  T e. _V
12 11 elpw2 
 |-  ( X e. ~P T <-> X C_ T )
13 12 biimpri 
 |-  ( X C_ T -> X e. ~P T )
14 13 adantl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> X e. ~P T )
15 fvex 
 |-  ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) e. _V
16 sseq1 
 |-  ( x = X -> ( x C_ z <-> X C_ z ) )
17 16 rabbidv 
 |-  ( x = X -> { z e. ran I | x C_ z } = { z e. ran I | X C_ z } )
18 17 inteqd 
 |-  ( x = X -> |^| { z e. ran I | x C_ z } = |^| { z e. ran I | X C_ z } )
19 18 fveq2d 
 |-  ( x = X -> ( `' I ` |^| { z e. ran I | x C_ z } ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
20 19 fveq2d 
 |-  ( x = X -> ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) = ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) )
21 20 oveq1d 
 |-  ( x = X -> ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) = ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) )
22 21 fvoveq1d 
 |-  ( x = X -> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
23 eqid 
 |-  ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
24 22 23 fvmptg 
 |-  ( ( X e. ~P T /\ ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) e. _V ) -> ( ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
25 14 15 24 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
26 10 25 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( N ` X ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )