Metamath Proof Explorer

Theorem dihatexv

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

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

Proof

Step Hyp Ref Expression
1 dihatexv.b 
 |-  B = ( Base ` K )
2 dihatexv.a 
 |-  A = ( Atoms ` K )
3 dihatexv.h 
 |-  H = ( LHyp ` K )
4 dihatexv.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihatexv.v 
 |-  V = ( Base ` U )
6 dihatexv.o 
 |-  .0. = ( 0g ` U )
7 dihatexv.n 
 |-  N = ( LSpan ` U )
8 dihatexv.i 
 |-  I = ( ( DIsoH ` K ) ` W )
9 dihatexv.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 dihatexv.q 
 |-  ( ph -> Q e. B )
11 9 ad2antrr 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> ( K e. HL /\ W e. H ) )
12 simplr 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> Q e. A )
13 simpr 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> Q ( le ` K ) W )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
16 eqid 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) )
17 1 14 2 3 15 16 4 8 7 dih1dimb2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ Q ( le ` K ) W ) ) -> E. g e. ( ( LTrn ` K ) ` W ) ( g =/= ( _I |` B ) /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) )
18 11 12 13 17 syl12anc 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> E. g e. ( ( LTrn ` K ) ` W ) ( g =/= ( _I |` B ) /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) )
19 9 ad3antrrr 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> ( K e. HL /\ W e. H ) )
20 simpr 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> g e. ( ( LTrn ` K ) ` W ) )
21 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
22 1 3 15 21 16 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) )
23 19 22 syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) )
24 3 15 21 4 5 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( g e. ( ( LTrn ` K ) ` W ) /\ ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. e. V )
25 19 20 23 24 syl12anc 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. e. V )
26 sneq 
 |-  ( x = <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. -> { x } = { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } )
27 26 fveq2d 
 |-  ( x = <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. -> ( N ` { x } ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) )
28 27 rspceeqv 
 |-  ( ( <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. e. V /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
29 25 28 sylan 
 |-  ( ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
30 29 ex 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> ( ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) ) )
31 30 adantld 
 |-  ( ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) /\ g e. ( ( LTrn ` K ) ` W ) ) -> ( ( g =/= ( _I |` B ) /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) ) )
32 31 rexlimdva 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> ( E. g e. ( ( LTrn ` K ) ` W ) ( g =/= ( _I |` B ) /\ ( I ` Q ) = ( N ` { <. g , ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) >. } ) ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) ) )
33 18 32 mpd 
 |-  ( ( ( ph /\ Q e. A ) /\ Q ( le ` K ) W ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
34 9 ad2antrr 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( K e. HL /\ W e. H ) )
35 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
36 14 2 3 35 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
37 34 36 syl 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
38 simplr 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> Q e. A )
39 simpr 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> -. Q ( le ` K ) W )
40 eqid 
 |-  ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q )
41 14 2 3 15 40 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) /\ ( Q e. A /\ -. Q ( le ` K ) W ) ) -> ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
42 34 37 38 39 41 syl112anc 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
43 3 15 21 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) )
44 34 43 syl 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) )
45 3 15 21 4 5 dvhelvbasei 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) /\ ( _I |` ( ( LTrn ` K ) ` W ) ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. V )
46 34 42 44 45 syl12anc 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. V )
47 14 2 3 35 15 8 4 7 40 dih1dimc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q ( le ` K ) W ) ) -> ( I ` Q ) = ( N ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
48 34 38 39 47 syl12anc 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> ( I ` Q ) = ( N ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
49 sneq 
 |-  ( x = <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. -> { x } = { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } )
50 49 fveq2d 
 |-  ( x = <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. -> ( N ` { x } ) = ( N ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
51 50 rspceeqv 
 |-  ( ( <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. V /\ ( I ` Q ) = ( N ` { <. ( iota_ f e. ( ( LTrn ` K ) ` W ) ( f ` ( ( oc ` K ) ` W ) ) = Q ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
52 46 48 51 syl2anc 
 |-  ( ( ( ph /\ Q e. A ) /\ -. Q ( le ` K ) W ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
53 33 52 pm2.61dan 
 |-  ( ( ph /\ Q e. A ) -> E. x e. V ( I ` Q ) = ( N ` { x } ) )
54 9 simpld 
 |-  ( ph -> K e. HL )
55 54 ad3antrrr 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> K e. HL )
56 hlatl 
 |-  ( K e. HL -> K e. AtLat )
57 55 56 syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> K e. AtLat )
58 simpllr 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> Q e. A )
59 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
60 59 2 atn0 
 |-  ( ( K e. AtLat /\ Q e. A ) -> Q =/= ( 0. ` K ) )
61 57 58 60 syl2anc 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> Q =/= ( 0. ` K ) )
62 sneq 
 |-  ( x = .0. -> { x } = { .0. } )
63 62 fveq2d 
 |-  ( x = .0. -> ( N ` { x } ) = ( N ` { .0. } ) )
64 63 3ad2ant3 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( N ` { x } ) = ( N ` { .0. } ) )
65 simp1ll 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ph )
66 3 4 9 dvhlmod 
 |-  ( ph -> U e. LMod )
67 6 7 lspsn0 
 |-  ( U e. LMod -> ( N ` { .0. } ) = { .0. } )
68 65 66 67 3syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( N ` { .0. } ) = { .0. } )
69 64 68 eqtrd 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( N ` { x } ) = { .0. } )
70 simp2 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( I ` Q ) = ( N ` { x } ) )
71 59 3 8 4 6 dih0 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) = { .0. } )
72 65 9 71 3syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( I ` ( 0. ` K ) ) = { .0. } )
73 69 70 72 3eqtr4d 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( I ` Q ) = ( I ` ( 0. ` K ) ) )
74 65 9 syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( K e. HL /\ W e. H ) )
75 65 10 syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> Q e. B )
76 65 54 syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> K e. HL )
77 hlop 
 |-  ( K e. HL -> K e. OP )
78 1 59 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. B )
79 76 77 78 3syl 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( 0. ` K ) e. B )
80 1 3 8 dih11 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. B /\ ( 0. ` K ) e. B ) -> ( ( I ` Q ) = ( I ` ( 0. ` K ) ) <-> Q = ( 0. ` K ) ) )
81 74 75 79 80 syl3anc 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> ( ( I ` Q ) = ( I ` ( 0. ` K ) ) <-> Q = ( 0. ` K ) ) )
82 73 81 mpbid 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) /\ x = .0. ) -> Q = ( 0. ` K ) )
83 82 3expia 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> ( x = .0. -> Q = ( 0. ` K ) ) )
84 83 necon3d 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> ( Q =/= ( 0. ` K ) -> x =/= .0. ) )
85 61 84 mpd 
 |-  ( ( ( ( ph /\ Q e. A ) /\ x e. V ) /\ ( I ` Q ) = ( N ` { x } ) ) -> x =/= .0. )
86 85 ex 
 |-  ( ( ( ph /\ Q e. A ) /\ x e. V ) -> ( ( I ` Q ) = ( N ` { x } ) -> x =/= .0. ) )
87 86 ancrd 
 |-  ( ( ( ph /\ Q e. A ) /\ x e. V ) -> ( ( I ` Q ) = ( N ` { x } ) -> ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) )
88 87 reximdva 
 |-  ( ( ph /\ Q e. A ) -> ( E. x e. V ( I ` Q ) = ( N ` { x } ) -> E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) )
89 53 88 mpd 
 |-  ( ( ph /\ Q e. A ) -> E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) )
90 89 ex 
 |-  ( ph -> ( Q e. A -> E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) )
91 9 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> ( K e. HL /\ W e. H ) )
92 10 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> Q e. B )
93 1 3 8 dihcnvid1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. B ) -> ( `' I ` ( I ` Q ) ) = Q )
94 91 92 93 syl2anc 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> ( `' I ` ( I ` Q ) ) = Q )
95 fveq2 
 |-  ( ( I ` Q ) = ( N ` { x } ) -> ( `' I ` ( I ` Q ) ) = ( `' I ` ( N ` { x } ) ) )
96 95 ad2antll 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> ( `' I ` ( I ` Q ) ) = ( `' I ` ( N ` { x } ) ) )
97 94 96 eqtr3d 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> Q = ( `' I ` ( N ` { x } ) ) )
98 66 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> U e. LMod )
99 simplr 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> x e. V )
100 simprl 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> x =/= .0. )
101 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
102 5 7 6 101 lsatlspsn2 
 |-  ( ( U e. LMod /\ x e. V /\ x =/= .0. ) -> ( N ` { x } ) e. ( LSAtoms ` U ) )
103 98 99 100 102 syl3anc 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> ( N ` { x } ) e. ( LSAtoms ` U ) )
104 2 3 4 8 101 dihlatat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { x } ) e. ( LSAtoms ` U ) ) -> ( `' I ` ( N ` { x } ) ) e. A )
105 91 103 104 syl2anc 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> ( `' I ` ( N ` { x } ) ) e. A )
106 97 105 eqeltrd 
 |-  ( ( ( ph /\ x e. V ) /\ ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) -> Q e. A )
107 106 ex 
 |-  ( ( ph /\ x e. V ) -> ( ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) -> Q e. A ) )
108 107 rexlimdva 
 |-  ( ph -> ( E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) -> Q e. A ) )
109 90 108 impbid 
 |-  ( ph -> ( Q e. A <-> E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) ) )
110 rexdifsn 
 |-  ( E. x e. ( V \ { .0. } ) ( I ` Q ) = ( N ` { x } ) <-> E. x e. V ( x =/= .0. /\ ( I ` Q ) = ( N ` { x } ) ) )
111 109 110 bitr4di 
 |-  ( ph -> ( Q e. A <-> E. x e. ( V \ { .0. } ) ( I ` Q ) = ( N ` { x } ) ) )