Metamath Proof Explorer

Theorem lcfrlem9

Description: Lemma for lcf1o . (This part has undesirable $d's on J and ph that we remove in lcf1o .) TODO: ugly proof; maybe have better subtheorems or abbreviate some iota_ k expansions with Jz ? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-2015)

Ref Expression
Hypotheses lcf1o.h 
|- H = ( LHyp ` K )
lcf1o.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcf1o.u 
|- U = ( ( DVecH ` K ) ` W )
lcf1o.v 
|- V = ( Base ` U )
lcf1o.a 
|- .+ = ( +g ` U )
lcf1o.t 
|- .x. = ( .s ` U )
lcf1o.s 
|- S = ( Scalar ` U )
lcf1o.r 
|- R = ( Base ` S )
lcf1o.z 
|- .0. = ( 0g ` U )
lcf1o.f 
|- F = ( LFnl ` U )
lcf1o.l 
|- L = ( LKer ` U )
lcf1o.d 
|- D = ( LDual ` U )
lcf1o.q 
|- Q = ( 0g ` D )
lcf1o.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcf1o.j 
|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
lcflo.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcfrlem9 
|- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )

Proof

Step Hyp Ref Expression
1 lcf1o.h 
 |-  H = ( LHyp ` K )
2 lcf1o.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcf1o.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcf1o.v 
 |-  V = ( Base ` U )
5 lcf1o.a 
 |-  .+ = ( +g ` U )
6 lcf1o.t 
 |-  .x. = ( .s ` U )
7 lcf1o.s 
 |-  S = ( Scalar ` U )
8 lcf1o.r 
 |-  R = ( Base ` S )
9 lcf1o.z 
 |-  .0. = ( 0g ` U )
10 lcf1o.f 
 |-  F = ( LFnl ` U )
11 lcf1o.l 
 |-  L = ( LKer ` U )
12 lcf1o.d 
 |-  D = ( LDual ` U )
13 lcf1o.q 
 |-  Q = ( 0g ` D )
14 lcf1o.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
15 lcf1o.j 
 |-  J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
16 lcflo.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
17 4 fvexi 
 |-  V e. _V
18 17 mptex 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) e. _V
19 18 15 fnmpti 
 |-  J Fn ( V \ { .0. } )
20 19 a1i 
 |-  ( ph -> J Fn ( V \ { .0. } ) )
21 fvelrnb 
 |-  ( J Fn ( V \ { .0. } ) -> ( g e. ran J <-> E. z e. ( V \ { .0. } ) ( J ` z ) = g ) )
22 20 21 syl 
 |-  ( ph -> ( g e. ran J <-> E. z e. ( V \ { .0. } ) ( J ` z ) = g ) )
23 16 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
24 simpr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> z e. ( V \ { .0. } ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24 lcfrlem8 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( J ` z ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
26 eqid 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) )
27 sneq 
 |-  ( y = z -> { y } = { z } )
28 27 fveq2d 
 |-  ( y = z -> ( ._|_ ` { y } ) = ( ._|_ ` { z } ) )
29 oveq2 
 |-  ( y = z -> ( k .x. y ) = ( k .x. z ) )
30 29 oveq2d 
 |-  ( y = z -> ( w .+ ( k .x. y ) ) = ( w .+ ( k .x. z ) ) )
31 30 eqeq2d 
 |-  ( y = z -> ( v = ( w .+ ( k .x. y ) ) <-> v = ( w .+ ( k .x. z ) ) ) )
32 28 31 rexeqbidv 
 |-  ( y = z -> ( E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) <-> E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) )
33 32 riotabidv 
 |-  ( y = z -> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) )
34 33 mpteq2dv 
 |-  ( y = z -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
35 34 rspceeqv 
 |-  ( ( z e. ( V \ { .0. } ) /\ ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) -> E. y e. ( V \ { .0. } ) ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) )
36 24 26 35 sylancl 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> E. y e. ( V \ { .0. } ) ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) )
37 36 olcd 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) = V \/ E. y e. ( V \ { .0. } ) ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) )
38 1 2 3 4 9 5 6 10 7 8 26 23 24 dochflcl 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. F )
39 1 2 3 4 5 6 7 8 9 10 11 14 23 38 lcfl6 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. C <-> ( ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) = V \/ E. y e. ( V \ { .0. } ) ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) )
40 37 39 mpbird 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. C )
41 1 2 3 4 9 5 6 11 7 8 26 23 24 dochsnkr2cl 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> z e. ( ( ._|_ ` ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) ) \ { .0. } ) )
42 1 2 3 4 9 10 11 23 38 41 dochsnkrlem3 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) ) ) = ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
43 1 2 3 4 9 10 11 23 38 41 dochsnkrlem1 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) ) ) =/= V )
44 42 43 eqnetrrd 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) =/= V )
45 1 3 16 dvhlmod 
 |-  ( ph -> U e. LMod )
46 45 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> U e. LMod )
47 4 10 11 12 13 46 38 lkr0f2 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) = V <-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) = Q ) )
48 47 necon3bid 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) =/= V <-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) =/= Q ) )
49 44 48 mpbid 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) =/= Q )
50 eldifsn 
 |-  ( ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. ( C \ { Q } ) <-> ( ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. C /\ ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) =/= Q ) )
51 40 49 50 sylanbrc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) e. ( C \ { Q } ) )
52 25 51 eqeltrd 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( J ` z ) e. ( C \ { Q } ) )
53 eleq1 
 |-  ( ( J ` z ) = g -> ( ( J ` z ) e. ( C \ { Q } ) <-> g e. ( C \ { Q } ) ) )
54 52 53 syl5ibcom 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( J ` z ) = g -> g e. ( C \ { Q } ) ) )
55 54 rexlimdva 
 |-  ( ph -> ( E. z e. ( V \ { .0. } ) ( J ` z ) = g -> g e. ( C \ { Q } ) ) )
56 eldifsn 
 |-  ( g e. ( C \ { Q } ) <-> ( g e. C /\ g =/= Q ) )
57 simprl 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> g e. C )
58 45 adantr 
 |-  ( ( ph /\ g e. C ) -> U e. LMod )
59 14 lcfl1lem 
 |-  ( g e. C <-> ( g e. F /\ ( ._|_ ` ( ._|_ ` ( L ` g ) ) ) = ( L ` g ) ) )
60 59 simplbi 
 |-  ( g e. C -> g e. F )
61 60 adantl 
 |-  ( ( ph /\ g e. C ) -> g e. F )
62 4 10 11 12 13 58 61 lkr0f2 
 |-  ( ( ph /\ g e. C ) -> ( ( L ` g ) = V <-> g = Q ) )
63 62 necon3bid 
 |-  ( ( ph /\ g e. C ) -> ( ( L ` g ) =/= V <-> g =/= Q ) )
64 63 biimprd 
 |-  ( ( ph /\ g e. C ) -> ( g =/= Q -> ( L ` g ) =/= V ) )
65 64 impr 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> ( L ` g ) =/= V )
66 65 neneqd 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> -. ( L ` g ) = V )
67 16 adantr 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> ( K e. HL /\ W e. H ) )
68 60 adantr 
 |-  ( ( g e. C /\ g =/= Q ) -> g e. F )
69 68 adantl 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> g e. F )
70 1 2 3 4 5 6 7 8 9 10 11 14 67 69 lcfl6 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> ( g e. C <-> ( ( L ` g ) = V \/ E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) ) )
71 70 biimpa 
 |-  ( ( ( ph /\ ( g e. C /\ g =/= Q ) ) /\ g e. C ) -> ( ( L ` g ) = V \/ E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
72 71 ord 
 |-  ( ( ( ph /\ ( g e. C /\ g =/= Q ) ) /\ g e. C ) -> ( -. ( L ` g ) = V -> E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
73 72 3impia 
 |-  ( ( ( ph /\ ( g e. C /\ g =/= Q ) ) /\ g e. C /\ -. ( L ` g ) = V ) -> E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
74 57 66 73 mpd3an23 
 |-  ( ( ph /\ ( g e. C /\ g =/= Q ) ) -> E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
75 56 74 sylan2b 
 |-  ( ( ph /\ g e. ( C \ { Q } ) ) -> E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
76 eqcom 
 |-  ( ( J ` z ) = g <-> g = ( J ` z ) )
77 16 ad2antrr 
 |-  ( ( ( ph /\ g e. ( C \ { Q } ) ) /\ z e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
78 simpr 
 |-  ( ( ( ph /\ g e. ( C \ { Q } ) ) /\ z e. ( V \ { .0. } ) ) -> z e. ( V \ { .0. } ) )
79 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 77 78 lcfrlem8 
 |-  ( ( ( ph /\ g e. ( C \ { Q } ) ) /\ z e. ( V \ { .0. } ) ) -> ( J ` z ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) )
80 79 eqeq2d 
 |-  ( ( ( ph /\ g e. ( C \ { Q } ) ) /\ z e. ( V \ { .0. } ) ) -> ( g = ( J ` z ) <-> g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
81 76 80 syl5bb 
 |-  ( ( ( ph /\ g e. ( C \ { Q } ) ) /\ z e. ( V \ { .0. } ) ) -> ( ( J ` z ) = g <-> g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
82 81 rexbidva 
 |-  ( ( ph /\ g e. ( C \ { Q } ) ) -> ( E. z e. ( V \ { .0. } ) ( J ` z ) = g <-> E. z e. ( V \ { .0. } ) g = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { z } ) v = ( w .+ ( k .x. z ) ) ) ) ) )
83 75 82 mpbird 
 |-  ( ( ph /\ g e. ( C \ { Q } ) ) -> E. z e. ( V \ { .0. } ) ( J ` z ) = g )
84 83 ex 
 |-  ( ph -> ( g e. ( C \ { Q } ) -> E. z e. ( V \ { .0. } ) ( J ` z ) = g ) )
85 55 84 impbid 
 |-  ( ph -> ( E. z e. ( V \ { .0. } ) ( J ` z ) = g <-> g e. ( C \ { Q } ) ) )
86 22 85 bitrd 
 |-  ( ph -> ( g e. ran J <-> g e. ( C \ { Q } ) ) )
87 86 eqrdv 
 |-  ( ph -> ran J = ( C \ { Q } ) )
88 16 ad2antrr 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> ( K e. HL /\ W e. H ) )
89 eqid 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { t } ) v = ( w .+ ( k .x. t ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { t } ) v = ( w .+ ( k .x. t ) ) ) )
90 eqid 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { u } ) v = ( w .+ ( k .x. u ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { u } ) v = ( w .+ ( k .x. u ) ) ) )
91 simplrl 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> t e. ( V \ { .0. } ) )
92 simplrr 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> u e. ( V \ { .0. } ) )
93 simpr 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> ( J ` t ) = ( J ` u ) )
94 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 91 lcfrlem8 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> ( J ` t ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { t } ) v = ( w .+ ( k .x. t ) ) ) ) )
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 92 lcfrlem8 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> ( J ` u ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { u } ) v = ( w .+ ( k .x. u ) ) ) ) )
96 93 94 95 3eqtr3d 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { t } ) v = ( w .+ ( k .x. t ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { u } ) v = ( w .+ ( k .x. u ) ) ) ) )
97 1 2 3 4 5 6 7 8 9 10 11 88 89 90 91 92 96 lcfl7lem 
 |-  ( ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) /\ ( J ` t ) = ( J ` u ) ) -> t = u )
98 97 ex 
 |-  ( ( ph /\ ( t e. ( V \ { .0. } ) /\ u e. ( V \ { .0. } ) ) ) -> ( ( J ` t ) = ( J ` u ) -> t = u ) )
99 98 ralrimivva 
 |-  ( ph -> A. t e. ( V \ { .0. } ) A. u e. ( V \ { .0. } ) ( ( J ` t ) = ( J ` u ) -> t = u ) )
100 dff1o6 
 |-  ( J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) <-> ( J Fn ( V \ { .0. } ) /\ ran J = ( C \ { Q } ) /\ A. t e. ( V \ { .0. } ) A. u e. ( V \ { .0. } ) ( ( J ` t ) = ( J ` u ) -> t = u ) ) )
101 20 87 99 100 syl3anbrc 
 |-  ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )