Metamath Proof Explorer

Theorem dochexmidlem1

Description: Lemma for dochexmid . Holland's proof implicitly requires q =/= r , which we prove here. (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h 
|- H = ( LHyp ` K )
dochexmidlem1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochexmidlem1.u 
|- U = ( ( DVecH ` K ) ` W )
dochexmidlem1.v 
|- V = ( Base ` U )
dochexmidlem1.s 
|- S = ( LSubSp ` U )
dochexmidlem1.n 
|- N = ( LSpan ` U )
dochexmidlem1.p 
|- .(+) = ( LSSum ` U )
dochexmidlem1.a 
|- A = ( LSAtoms ` U )
dochexmidlem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochexmidlem1.x 
|- ( ph -> X e. S )
dochexmidlem1.pp 
|- ( ph -> p e. A )
dochexmidlem1.qq 
|- ( ph -> q e. A )
dochexmidlem1.rr 
|- ( ph -> r e. A )
dochexmidlem1.ql 
|- ( ph -> q C_ ( ._|_ ` X ) )
dochexmidlem1.rl 
|- ( ph -> r C_ X )
Assertion dochexmidlem1 
|- ( ph -> q =/= r )

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h 
 |-  H = ( LHyp ` K )
2 dochexmidlem1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochexmidlem1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochexmidlem1.v 
 |-  V = ( Base ` U )
5 dochexmidlem1.s 
 |-  S = ( LSubSp ` U )
6 dochexmidlem1.n 
 |-  N = ( LSpan ` U )
7 dochexmidlem1.p 
 |-  .(+) = ( LSSum ` U )
8 dochexmidlem1.a 
 |-  A = ( LSAtoms ` U )
9 dochexmidlem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 dochexmidlem1.x 
 |-  ( ph -> X e. S )
11 dochexmidlem1.pp 
 |-  ( ph -> p e. A )
12 dochexmidlem1.qq 
 |-  ( ph -> q e. A )
13 dochexmidlem1.rr 
 |-  ( ph -> r e. A )
14 dochexmidlem1.ql 
 |-  ( ph -> q C_ ( ._|_ ` X ) )
15 dochexmidlem1.rl 
 |-  ( ph -> r C_ X )
16 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
17 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
18 16 8 17 13 lsatn0 
 |-  ( ph -> r =/= { ( 0g ` U ) } )
19 5 8 17 13 lsatlssel 
 |-  ( ph -> r e. S )
20 16 5 lssle0 
 |-  ( ( U e. LMod /\ r e. S ) -> ( r C_ { ( 0g ` U ) } <-> r = { ( 0g ` U ) } ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ( r C_ { ( 0g ` U ) } <-> r = { ( 0g ` U ) } ) )
22 21 necon3bbid 
 |-  ( ph -> ( -. r C_ { ( 0g ` U ) } <-> r =/= { ( 0g ` U ) } ) )
23 18 22 mpbird 
 |-  ( ph -> -. r C_ { ( 0g ` U ) } )
24 1 3 5 16 2 dochnoncon 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S ) -> ( X i^i ( ._|_ ` X ) ) = { ( 0g ` U ) } )
25 9 10 24 syl2anc 
 |-  ( ph -> ( X i^i ( ._|_ ` X ) ) = { ( 0g ` U ) } )
26 25 sseq2d 
 |-  ( ph -> ( r C_ ( X i^i ( ._|_ ` X ) ) <-> r C_ { ( 0g ` U ) } ) )
27 23 26 mtbird 
 |-  ( ph -> -. r C_ ( X i^i ( ._|_ ` X ) ) )
28 sseq1 
 |-  ( q = r -> ( q C_ ( ._|_ ` X ) <-> r C_ ( ._|_ ` X ) ) )
29 14 28 syl5ibcom 
 |-  ( ph -> ( q = r -> r C_ ( ._|_ ` X ) ) )
30 29 15 jctild 
 |-  ( ph -> ( q = r -> ( r C_ X /\ r C_ ( ._|_ ` X ) ) ) )
31 ssin 
 |-  ( ( r C_ X /\ r C_ ( ._|_ ` X ) ) <-> r C_ ( X i^i ( ._|_ ` X ) ) )
32 30 31 syl6ib 
 |-  ( ph -> ( q = r -> r C_ ( X i^i ( ._|_ ` X ) ) ) )
33 32 necon3bd 
 |-  ( ph -> ( -. r C_ ( X i^i ( ._|_ ` X ) ) -> q =/= r ) )
34 27 33 mpd 
 |-  ( ph -> q =/= r )