Metamath Proof Explorer

Theorem dihatexv2

Description: There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses dihatexv2.a 
|- A = ( Atoms ` K )
dihatexv2.h 
|- H = ( LHyp ` K )
dihatexv2.u 
|- U = ( ( DVecH ` K ) ` W )
dihatexv2.v 
|- V = ( Base ` U )
dihatexv2.o 
|- .0. = ( 0g ` U )
dihatexv2.n 
|- N = ( LSpan ` U )
dihatexv2.i 
|- I = ( ( DIsoH ` K ) ` W )
dihatexv2.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dihatexv2 
|- ( ph -> ( Q e. A <-> E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) ) )

Proof

Step Hyp Ref Expression
1 dihatexv2.a 
 |-  A = ( Atoms ` K )
2 dihatexv2.h 
 |-  H = ( LHyp ` K )
3 dihatexv2.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dihatexv2.v 
 |-  V = ( Base ` U )
5 dihatexv2.o 
 |-  .0. = ( 0g ` U )
6 dihatexv2.n 
 |-  N = ( LSpan ` U )
7 dihatexv2.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihatexv2.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 1 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
11 10 anim2i 
 |-  ( ( ph /\ Q e. A ) -> ( ph /\ Q e. ( Base ` K ) ) )
12 8 adantr 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
13 eldifi 
 |-  ( x e. ( V \ { .0. } ) -> x e. V )
14 2 3 4 6 7 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. V ) -> ( N ` { x } ) e. ran I )
15 8 13 14 syl2an 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( N ` { x } ) e. ran I )
16 9 2 7 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { x } ) e. ran I ) -> ( `' I ` ( N ` { x } ) ) e. ( Base ` K ) )
17 12 15 16 syl2anc 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( `' I ` ( N ` { x } ) ) e. ( Base ` K ) )
18 eleq1a 
 |-  ( ( `' I ` ( N ` { x } ) ) e. ( Base ` K ) -> ( Q = ( `' I ` ( N ` { x } ) ) -> Q e. ( Base ` K ) ) )
19 17 18 syl 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( Q = ( `' I ` ( N ` { x } ) ) -> Q e. ( Base ` K ) ) )
20 19 rexlimdva 
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) -> Q e. ( Base ` K ) ) )
21 20 imdistani 
 |-  ( ( ph /\ E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) ) -> ( ph /\ Q e. ( Base ` K ) ) )
22 8 adantr 
 |-  ( ( ph /\ Q e. ( Base ` K ) ) -> ( K e. HL /\ W e. H ) )
23 simpr 
 |-  ( ( ph /\ Q e. ( Base ` K ) ) -> Q e. ( Base ` K ) )
24 9 1 2 3 4 5 6 7 22 23 dihatexv 
 |-  ( ( ph /\ Q e. ( Base ` K ) ) -> ( Q e. A <-> E. x e. ( V \ { .0. } ) ( I ` Q ) = ( N ` { x } ) ) )
25 22 adantr 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
26 22 13 14 syl2an 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( N ` { x } ) e. ran I )
27 2 7 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { x } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { x } ) ) ) = ( N ` { x } ) )
28 25 26 27 syl2anc 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( I ` ( `' I ` ( N ` { x } ) ) ) = ( N ` { x } ) )
29 28 eqeq2d 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( ( I ` Q ) = ( I ` ( `' I ` ( N ` { x } ) ) ) <-> ( I ` Q ) = ( N ` { x } ) ) )
30 simplr 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> Q e. ( Base ` K ) )
31 25 26 16 syl2anc 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( `' I ` ( N ` { x } ) ) e. ( Base ` K ) )
32 9 2 7 dih11 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. ( Base ` K ) /\ ( `' I ` ( N ` { x } ) ) e. ( Base ` K ) ) -> ( ( I ` Q ) = ( I ` ( `' I ` ( N ` { x } ) ) ) <-> Q = ( `' I ` ( N ` { x } ) ) ) )
33 25 30 31 32 syl3anc 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( ( I ` Q ) = ( I ` ( `' I ` ( N ` { x } ) ) ) <-> Q = ( `' I ` ( N ` { x } ) ) ) )
34 29 33 bitr3d 
 |-  ( ( ( ph /\ Q e. ( Base ` K ) ) /\ x e. ( V \ { .0. } ) ) -> ( ( I ` Q ) = ( N ` { x } ) <-> Q = ( `' I ` ( N ` { x } ) ) ) )
35 34 rexbidva 
 |-  ( ( ph /\ Q e. ( Base ` K ) ) -> ( E. x e. ( V \ { .0. } ) ( I ` Q ) = ( N ` { x } ) <-> E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) ) )
36 24 35 bitrd 
 |-  ( ( ph /\ Q e. ( Base ` K ) ) -> ( Q e. A <-> E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) ) )
37 11 21 36 pm5.21nd 
 |-  ( ph -> ( Q e. A <-> E. x e. ( V \ { .0. } ) Q = ( `' I ` ( N ` { x } ) ) ) )