Metamath Proof Explorer

Theorem docaffvalN

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 )
Assertion 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 ) ) ) ) )

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 elex 
 |-  ( K e. V -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
7 6 4 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
8 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
9 8 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
10 9 pweqd 
 |-  ( k = K -> ~P ( ( LTrn ` k ) ` w ) = ~P ( ( LTrn ` K ) ` w ) )
11 fveq2 
 |-  ( k = K -> ( DIsoA ` k ) = ( DIsoA ` K ) )
12 11 fveq1d 
 |-  ( k = K -> ( ( DIsoA ` k ) ` w ) = ( ( DIsoA ` K ) ` w ) )
13 fveq2 
 |-  ( k = K -> ( meet ` k ) = ( meet ` K ) )
14 13 2 eqtr4di 
 |-  ( k = K -> ( meet ` k ) = ./\ )
15 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
16 15 1 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
17 fveq2 
 |-  ( k = K -> ( oc ` k ) = ( oc ` K ) )
18 17 3 eqtr4di 
 |-  ( k = K -> ( oc ` k ) = ._|_ )
19 12 cnveqd 
 |-  ( k = K -> `' ( ( DIsoA ` k ) ` w ) = `' ( ( DIsoA ` K ) ` w ) )
20 12 rneqd 
 |-  ( k = K -> ran ( ( DIsoA ` k ) ` w ) = ran ( ( DIsoA ` K ) ` w ) )
21 20 rabeqdv 
 |-  ( k = K -> { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } = { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } )
22 21 inteqd 
 |-  ( k = K -> |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } = |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } )
23 19 22 fveq12d 
 |-  ( k = K -> ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) = ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) )
24 18 23 fveq12d 
 |-  ( k = K -> ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) = ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) )
25 18 fveq1d 
 |-  ( k = K -> ( ( oc ` k ) ` w ) = ( ._|_ ` w ) )
26 16 24 25 oveq123d 
 |-  ( k = K -> ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) = ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) )
27 eqidd 
 |-  ( k = K -> w = w )
28 14 26 27 oveq123d 
 |-  ( k = K -> ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) = ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) )
29 12 28 fveq12d 
 |-  ( k = K -> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) = ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) )
30 10 29 mpteq12dv 
 |-  ( k = K -> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) = ( x e. ~P ( ( LTrn ` K ) ` w ) |-> ( ( ( DIsoA ` K ) ` w ) ` ( ( ( ._|_ ` ( `' ( ( DIsoA ` K ) ` w ) ` |^| { z e. ran ( ( DIsoA ` K ) ` w ) | x C_ z } ) ) .\/ ( ._|_ ` w ) ) ./\ w ) ) ) )
31 7 30 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` 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 ) ) ) ) )
32 df-docaN 
 |-  ocA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ~P ( ( LTrn ` k ) ` w ) |-> ( ( ( DIsoA ` k ) ` w ) ` ( ( ( ( oc ` k ) ` ( `' ( ( DIsoA ` k ) ` w ) ` |^| { z e. ran ( ( DIsoA ` k ) ` w ) | x C_ z } ) ) ( join ` k ) ( ( oc ` k ) ` w ) ) ( meet ` k ) w ) ) ) ) )
33 31 32 4 mptfvmpt 
 |-  ( 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 ) ) ) ) )
34 5 33 syl 
 |-  ( 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 ) ) ) ) )