Metamath Proof Explorer

Theorem docaclN

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

Ref Expression
Hypotheses docacl.h 
|- H = ( LHyp ` K )
docacl.t 
|- T = ( ( LTrn ` K ) ` W )
docacl.i 
|- I = ( ( DIsoA ` K ) ` W )
docacl.n 
|- ._|_ = ( ( ocA ` K ) ` W )
Assertion docaclN 
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ._|_ ` X ) e. ran I )

Proof

Step Hyp Ref Expression
1 docacl.h 
 |-  H = ( LHyp ` K )
2 docacl.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 docacl.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 docacl.n 
 |-  ._|_ = ( ( ocA ` K ) ` W )
5 eqid 
 |-  ( join ` K ) = ( join ` K )
6 eqid 
 |-  ( meet ` K ) = ( meet ` K )
7 eqid 
 |-  ( oc ` K ) = ( oc ` K )
8 5 6 7 1 2 3 4 docavalN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ._|_ ` X ) = ( I ` ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
9 1 3 diaf11N 
 |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
10 f1ofun 
 |-  ( I : dom I -1-1-onto-> ran I -> Fun I )
11 9 10 syl 
 |-  ( ( K e. HL /\ W e. H ) -> Fun I )
12 11 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> Fun I )
13 hllat 
 |-  ( K e. HL -> K e. Lat )
14 13 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> K e. Lat )
15 hlop 
 |-  ( K e. HL -> K e. OP )
16 15 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> K e. OP )
17 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( K e. HL /\ W e. H ) )
18 ssrab2 
 |-  { z e. ran I | X C_ z } C_ ran I
19 18 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> { z e. ran I | X C_ z } C_ ran I )
20 1 2 3 dia1elN 
 |-  ( ( K e. HL /\ W e. H ) -> T e. ran I )
21 20 anim1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( T e. ran I /\ X C_ T ) )
22 sseq2 
 |-  ( z = T -> ( X C_ z <-> X C_ T ) )
23 22 elrab 
 |-  ( T e. { z e. ran I | X C_ z } <-> ( T e. ran I /\ X C_ T ) )
24 21 23 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> T e. { z e. ran I | X C_ z } )
25 24 ne0d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> { z e. ran I | X C_ z } =/= (/) )
26 1 3 diaintclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( { z e. ran I | X C_ z } C_ ran I /\ { z e. ran I | X C_ z } =/= (/) ) ) -> |^| { z e. ran I | X C_ z } e. ran I )
27 17 19 25 26 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> |^| { z e. ran I | X C_ z } e. ran I )
28 1 3 diacnvclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ |^| { z e. ran I | X C_ z } e. ran I ) -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. dom I )
29 27 28 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. dom I )
30 eqid 
 |-  ( Base ` K ) = ( Base ` K )
31 30 1 3 diadmclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` |^| { z e. ran I | X C_ z } ) e. dom I ) -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) )
32 29 31 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) )
33 30 7 opoccl 
 |-  ( ( K e. OP /\ ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) )
34 16 32 33 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) )
35 30 1 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
36 35 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> W e. ( Base ` K ) )
37 30 7 opoccl 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
38 16 36 37 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
39 30 5 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
40 14 34 38 39 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
41 30 6 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
42 14 40 36 41 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
43 eqid 
 |-  ( le ` K ) = ( le ` K )
44 30 43 6 latmle2 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
45 14 40 36 44 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
46 30 43 1 3 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
47 46 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
48 42 45 47 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I )
49 fvelrn 
 |-  ( ( Fun I /\ ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ran I )
50 12 48 49 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( I ` ( ( ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) e. ran I )
51 8 50 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ._|_ ` X ) e. ran I )