Metamath Proof Explorer

Theorem docafvalN

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 docafvalN 
|- ( ( K e. V /\ W e. H ) -> N = ( x e. ~P T |-> ( 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 docaffvalN 
 |-  ( K e. V -> ( ocA ` K ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) )
9 8 fveq1d 
 |-  ( K e. V -> ( ( ocA ` K ) ` W ) = ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) ` W ) )
10 7 9 syl5eq 
 |-  ( K e. V -> N = ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) ` W ) )
11 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
12 11 5 eqtr4di 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = T )
13 12 pweqd 
 |-  ( w = W -> ~P ( ( LTrn ` K ) ` w ) = ~P T )
14 fveq2 
 |-  ( w = W -> ( ( DIsoA ` K ) ` w ) = ( ( DIsoA ` K ) ` W ) )
15 14 6 eqtr4di 
 |-  ( w = W -> ( ( DIsoA ` K ) ` w ) = I )
16 15 cnveqd 
 |-  ( w = W -> `' ( ( DIsoA ` K ) ` w ) = `' I )
17 15 rneqd 
 |-  ( w = W -> ran ( ( DIsoA ` K ) ` w ) = ran I )
18 17 rabeqdv 
 |-  ( w = W -> { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } = { z e. ran I | x C_ z } )
19 18 inteqd 
 |-  ( w = W -> |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } = |^| { z e. ran I | x C_ z } )
20 16 19 fveq12d 
 |-  ( w = W -> ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) = ( `' I ` |^| { z e. ran I | x C_ z } ) )
21 20 fveq2d 
 |-  ( w = W -> ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) = ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) )
22 fveq2 
 |-  ( w = W -> ( ._|_ ` w ) = ( ._|_ ` W ) )
23 21 22 oveq12d 
 |-  ( w = W -> ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) = ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) )
24 id 
 |-  ( w = W -> w = W )
25 23 24 oveq12d 
 |-  ( w = W -> ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) = ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) )
26 15 25 fveq12d 
 |-  ( w = W -> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
27 13 26 mpteq12dv 
 |-  ( w = W -> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
28 eqid 
 |-  ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) = ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) )
29 5 fvexi 
 |-  T e. _V
30 29 pwex 
 |-  ~P T e. _V
31 30 mptex 
 |-  ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) e. _V
32 27 28 31 fvmpt 
 |-  ( W e. H -> ( ( w e. H |-> ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) ) ` W ) = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )
33 10 32 sylan9eq 
 |-  ( ( K e. V /\ W e. H ) -> N = ( x e. ~P T |-> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | x C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) ) )