Step |
Hyp |
Ref |
Expression |
1 |
|
lcfl6.h |
|- H = ( LHyp ` K ) |
2 |
|
lcfl6.o |
|- ._|_ = ( ( ocH ` K ) ` W ) |
3 |
|
lcfl6.u |
|- U = ( ( DVecH ` K ) ` W ) |
4 |
|
lcfl6.v |
|- V = ( Base ` U ) |
5 |
|
lcfl6.a |
|- .+ = ( +g ` U ) |
6 |
|
lcfl6.t |
|- .x. = ( .s ` U ) |
7 |
|
lcfl6.s |
|- S = ( Scalar ` U ) |
8 |
|
lcfl6.r |
|- R = ( Base ` S ) |
9 |
|
lcfl6.z |
|- .0. = ( 0g ` U ) |
10 |
|
lcfl6.f |
|- F = ( LFnl ` U ) |
11 |
|
lcfl6.l |
|- L = ( LKer ` U ) |
12 |
|
lcfl6.c |
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } |
13 |
|
lcfl6.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
14 |
|
lcfl6.g |
|- ( ph -> G e. F ) |
15 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14
|
lcfl6 |
|- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) ) |
16 |
13
|
ad2antrr |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> ( K e. HL /\ W e. H ) ) |
17 |
|
eqid |
|- ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) |
18 |
|
eqid |
|- ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) |
19 |
|
simplrl |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> x e. ( V \ { .0. } ) ) |
20 |
|
simplrr |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> y e. ( V \ { .0. } ) ) |
21 |
|
simprl |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) |
22 |
|
eqeq1 |
|- ( v = u -> ( v = ( w .+ ( k .x. x ) ) <-> u = ( w .+ ( k .x. x ) ) ) ) |
23 |
22
|
rexbidv |
|- ( v = u -> ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) ) |
24 |
23
|
riotabidv |
|- ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) ) |
25 |
|
oveq1 |
|- ( k = l -> ( k .x. x ) = ( l .x. x ) ) |
26 |
25
|
oveq2d |
|- ( k = l -> ( w .+ ( k .x. x ) ) = ( w .+ ( l .x. x ) ) ) |
27 |
26
|
eqeq2d |
|- ( k = l -> ( u = ( w .+ ( k .x. x ) ) <-> u = ( w .+ ( l .x. x ) ) ) ) |
28 |
27
|
rexbidv |
|- ( k = l -> ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { x } ) u = ( w .+ ( l .x. x ) ) ) ) |
29 |
|
oveq1 |
|- ( w = z -> ( w .+ ( l .x. x ) ) = ( z .+ ( l .x. x ) ) ) |
30 |
29
|
eqeq2d |
|- ( w = z -> ( u = ( w .+ ( l .x. x ) ) <-> u = ( z .+ ( l .x. x ) ) ) ) |
31 |
30
|
cbvrexvw |
|- ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( l .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) |
32 |
28 31
|
bitrdi |
|- ( k = l -> ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) |
33 |
32
|
cbvriotavw |
|- ( iota_ k e. R E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) |
34 |
24 33
|
eqtrdi |
|- ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) |
35 |
34
|
cbvmptv |
|- ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) |
36 |
21 35
|
eqtrdi |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) ) |
37 |
|
simprr |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) |
38 |
|
eqeq1 |
|- ( v = u -> ( v = ( w .+ ( k .x. y ) ) <-> u = ( w .+ ( k .x. y ) ) ) ) |
39 |
38
|
rexbidv |
|- ( v = u -> ( E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) <-> E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) ) |
40 |
39
|
riotabidv |
|- ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) ) |
41 |
|
oveq1 |
|- ( k = l -> ( k .x. y ) = ( l .x. y ) ) |
42 |
41
|
oveq2d |
|- ( k = l -> ( w .+ ( k .x. y ) ) = ( w .+ ( l .x. y ) ) ) |
43 |
42
|
eqeq2d |
|- ( k = l -> ( u = ( w .+ ( k .x. y ) ) <-> u = ( w .+ ( l .x. y ) ) ) ) |
44 |
43
|
rexbidv |
|- ( k = l -> ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) <-> E. w e. ( ._|_ ` { y } ) u = ( w .+ ( l .x. y ) ) ) ) |
45 |
|
oveq1 |
|- ( w = z -> ( w .+ ( l .x. y ) ) = ( z .+ ( l .x. y ) ) ) |
46 |
45
|
eqeq2d |
|- ( w = z -> ( u = ( w .+ ( l .x. y ) ) <-> u = ( z .+ ( l .x. y ) ) ) ) |
47 |
46
|
cbvrexvw |
|- ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( l .x. y ) ) <-> E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) |
48 |
44 47
|
bitrdi |
|- ( k = l -> ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) <-> E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) |
49 |
48
|
cbvriotavw |
|- ( iota_ k e. R E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) |
50 |
40 49
|
eqtrdi |
|- ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) |
51 |
50
|
cbvmptv |
|- ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) |
52 |
37 51
|
eqtrdi |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) ) |
53 |
36 52
|
eqtr3d |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) ) |
54 |
1 2 3 4 5 6 7 8 9 10 11 16 17 18 19 20 53
|
lcfl7lem |
|- ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> x = y ) |
55 |
54
|
ex |
|- ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) -> ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) |
56 |
55
|
ralrimivva |
|- ( ph -> A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) |
57 |
56
|
a1d |
|- ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) ) |
58 |
57
|
ancld |
|- ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) ) ) |
59 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
60 |
59
|
fveq2d |
|- ( x = y -> ( ._|_ ` { x } ) = ( ._|_ ` { y } ) ) |
61 |
|
oveq2 |
|- ( x = y -> ( k .x. x ) = ( k .x. y ) ) |
62 |
61
|
oveq2d |
|- ( x = y -> ( w .+ ( k .x. x ) ) = ( w .+ ( k .x. y ) ) ) |
63 |
62
|
eqeq2d |
|- ( x = y -> ( v = ( w .+ ( k .x. x ) ) <-> v = ( w .+ ( k .x. y ) ) ) ) |
64 |
60 63
|
rexeqbidv |
|- ( x = y -> ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) |
65 |
64
|
riotabidv |
|- ( x = y -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) |
66 |
65
|
mpteq2dv |
|- ( x = y -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) |
67 |
66
|
eqeq2d |
|- ( x = y -> ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) |
68 |
67
|
reu4 |
|- ( E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) ) |
69 |
58 68
|
syl6ibr |
|- ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) |
70 |
|
reurex |
|- ( E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) |
71 |
69 70
|
impbid1 |
|- ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) |
72 |
71
|
orbi2d |
|- ( ph -> ( ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) ) |
73 |
15 72
|
bitrd |
|- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) ) |