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 )