Metamath Proof Explorer

Theorem dochnoncon

Description: Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses dochnoncon.h 
|- H = ( LHyp ` K )
dochnoncon.u 
|- U = ( ( DVecH ` K ) ` W )
dochnoncon.s 
|- S = ( LSubSp ` U )
dochnoncon.z 
|- .0. = ( 0g ` U )
dochnoncon.o 
|- ._|_ = ( ( ocH ` K ) ` W )
Assertion dochnoncon 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 dochnoncon.h 
 |-  H = ( LHyp ` K )
2 dochnoncon.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dochnoncon.s 
 |-  S = ( LSubSp ` U )
4 dochnoncon.z 
 |-  .0. = ( 0g ` U )
5 dochnoncon.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
6 eqid 
 |-  ( Base ` U ) = ( Base ` U )
7 6 3 lssss 
 |-  ( X e. S -> X C_ ( Base ` U ) )
8 1 2 6 5 dochocss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` U ) ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
9 7 8 sylan2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
10 9 ssrind 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) C_ ( ( ._|_ ` ( ._|_ ` X ) ) i^i ( ._|_ ` X ) ) )
11 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( K e. HL /\ W e. H ) )
12 eqid 
 |-  ( Base ` K ) = ( Base ` K )
13 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
14 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
15 12 1 13 2 14 dihf11 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) )
16 15 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) )
17 f1f1orn 
 |-  ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) )
19 1 13 2 6 5 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` U ) ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
20 7 19 sylan2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
21 1 2 13 14 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
22 20 21 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
23 6 14 lssss 
 |-  ( ( ._|_ ` X ) e. ( LSubSp ` U ) -> ( ._|_ ` X ) C_ ( Base ` U ) )
24 22 23 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` X ) C_ ( Base ` U ) )
25 1 13 2 6 5 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ ( Base ` U ) ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
26 24 25 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
27 f1ocnvdm 
 |-  ( ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) /\ ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) e. ( Base ` K ) )
28 18 26 27 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) e. ( Base ` K ) )
29 hlop 
 |-  ( K e. HL -> K e. OP )
30 29 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> K e. OP )
31 eqid 
 |-  ( oc ` K ) = ( oc ` K )
32 12 31 opoccl 
 |-  ( ( K e. OP /\ ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) e. ( Base ` K ) )
33 30 28 32 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) e. ( Base ` K ) )
34 eqid 
 |-  ( meet ` K ) = ( meet ` K )
35 12 34 1 13 dihmeet 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) e. ( Base ` K ) /\ ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) e. ( Base ` K ) ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ( meet ` K ) ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) = ( ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) i^i ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) )
36 11 28 33 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ( meet ` K ) ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) = ( ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) i^i ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) )
37 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
38 12 31 34 37 opnoncon 
 |-  ( ( K e. OP /\ ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) e. ( Base ` K ) ) -> ( ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ( meet ` K ) ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) = ( 0. ` K ) )
39 30 28 38 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ( meet ` K ) ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) = ( 0. ` K ) )
40 39 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ( meet ` K ) ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( 0. ` K ) ) )
41 36 40 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) i^i ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( 0. ` K ) ) )
42 1 13 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
43 26 42 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
44 31 1 13 5 dochvalr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) )
45 26 44 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) )
46 1 13 5 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
47 20 46 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
48 45 47 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) = ( ._|_ ` X ) )
49 43 48 ineq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) i^i ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` ( ._|_ ` X ) ) ) ) ) ) = ( ( ._|_ ` ( ._|_ ` X ) ) i^i ( ._|_ ` X ) ) )
50 37 1 13 2 4 dih0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 0. ` K ) ) = { .0. } )
51 50 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 0. ` K ) ) = { .0. } )
52 41 49 51 3eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ( ._|_ ` ( ._|_ ` X ) ) i^i ( ._|_ ` X ) ) = { .0. } )
53 10 52 sseqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) C_ { .0. } )
54 1 2 11 dvhlmod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> U e. LMod )
55 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> X e. S )
56 1 2 13 3 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` X ) e. S )
57 20 56 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( ._|_ ` X ) e. S )
58 3 lssincl 
 |-  ( ( U e. LMod /\ X e. S /\ ( ._|_ ` X ) e. S ) -> ( X i^i ( ._|_ ` X ) ) e. S )
59 54 55 57 58 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) e. S )
60 4 3 lss0ss 
 |-  ( ( U e. LMod /\ ( X i^i ( ._|_ ` X ) ) e. S ) -> { .0. } C_ ( X i^i ( ._|_ ` X ) ) )
61 54 59 60 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> { .0. } C_ ( X i^i ( ._|_ ` X ) ) )
62 53 61 eqssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) = { .0. } )