Metamath Proof Explorer

Theorem dochfl1

Description: The value of the explicit functional G is 1 at the X that determines it. (Contributed by NM, 27-Oct-2014)

Ref Expression
Hypotheses dochfl1.h 
|- H = ( LHyp ` K )
dochfl1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochfl1.u 
|- U = ( ( DVecH ` K ) ` W )
dochfl1.v 
|- V = ( Base ` U )
dochfl1.a 
|- .+ = ( +g ` U )
dochfl1.t 
|- .x. = ( .s ` U )
dochfl1.z 
|- .0. = ( 0g ` U )
dochfl1.d 
|- D = ( Scalar ` U )
dochfl1.r 
|- R = ( Base ` D )
dochfl1.i 
|- .1. = ( 1r ` D )
dochfl1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochfl1.x 
|- ( ph -> X e. ( V \ { .0. } ) )
dochfl1.g 
|- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
Assertion dochfl1 
|- ( ph -> ( G ` X ) = .1. )

Proof

Step Hyp Ref Expression
1 dochfl1.h 
 |-  H = ( LHyp ` K )
2 dochfl1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochfl1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochfl1.v 
 |-  V = ( Base ` U )
5 dochfl1.a 
 |-  .+ = ( +g ` U )
6 dochfl1.t 
 |-  .x. = ( .s ` U )
7 dochfl1.z 
 |-  .0. = ( 0g ` U )
8 dochfl1.d 
 |-  D = ( Scalar ` U )
9 dochfl1.r 
 |-  R = ( Base ` D )
10 dochfl1.i 
 |-  .1. = ( 1r ` D )
11 dochfl1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 dochfl1.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
13 dochfl1.g 
 |-  G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
14 12 eldifad 
 |-  ( ph -> X e. V )
15 eqeq1 
 |-  ( v = X -> ( v = ( w .+ ( k .x. X ) ) <-> X = ( w .+ ( k .x. X ) ) ) )
16 15 rexbidv 
 |-  ( v = X -> ( E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) <-> E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) )
17 16 riotabidv 
 |-  ( v = X -> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) )
18 riotaex 
 |-  ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) e. _V
19 17 13 18 fvmpt 
 |-  ( X e. V -> ( G ` X ) = ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) )
20 14 19 syl 
 |-  ( ph -> ( G ` X ) = ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) )
21 1 3 11 dvhlmod 
 |-  ( ph -> U e. LMod )
22 14 snssd 
 |-  ( ph -> { X } C_ V )
23 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
24 1 3 4 23 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V ) -> ( ._|_ ` { X } ) e. ( LSubSp ` U ) )
25 11 22 24 syl2anc 
 |-  ( ph -> ( ._|_ ` { X } ) e. ( LSubSp ` U ) )
26 7 23 lss0cl 
 |-  ( ( U e. LMod /\ ( ._|_ ` { X } ) e. ( LSubSp ` U ) ) -> .0. e. ( ._|_ ` { X } ) )
27 21 25 26 syl2anc 
 |-  ( ph -> .0. e. ( ._|_ ` { X } ) )
28 4 8 6 10 lmodvs1 
 |-  ( ( U e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )
29 21 14 28 syl2anc 
 |-  ( ph -> ( .1. .x. X ) = X )
30 29 oveq2d 
 |-  ( ph -> ( .0. .+ ( .1. .x. X ) ) = ( .0. .+ X ) )
31 4 5 7 lmod0vlid 
 |-  ( ( U e. LMod /\ X e. V ) -> ( .0. .+ X ) = X )
32 21 14 31 syl2anc 
 |-  ( ph -> ( .0. .+ X ) = X )
33 30 32 eqtr2d 
 |-  ( ph -> X = ( .0. .+ ( .1. .x. X ) ) )
34 oveq1 
 |-  ( w = .0. -> ( w .+ ( .1. .x. X ) ) = ( .0. .+ ( .1. .x. X ) ) )
35 34 rspceeqv 
 |-  ( ( .0. e. ( ._|_ ` { X } ) /\ X = ( .0. .+ ( .1. .x. X ) ) ) -> E. w e. ( ._|_ ` { X } ) X = ( w .+ ( .1. .x. X ) ) )
36 27 33 35 syl2anc 
 |-  ( ph -> E. w e. ( ._|_ ` { X } ) X = ( w .+ ( .1. .x. X ) ) )
37 8 lmodring 
 |-  ( U e. LMod -> D e. Ring )
38 9 10 ringidcl 
 |-  ( D e. Ring -> .1. e. R )
39 21 37 38 3syl 
 |-  ( ph -> .1. e. R )
40 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
41 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
42 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
43 1 3 11 dvhlvec 
 |-  ( ph -> U e. LVec )
44 1 2 3 4 7 42 11 12 dochsnshp 
 |-  ( ph -> ( ._|_ ` { X } ) e. ( LSHyp ` U ) )
45 1 2 3 4 7 40 41 11 12 dochexmidat 
 |-  ( ph -> ( ( ._|_ ` { X } ) ( LSSum ` U ) ( ( LSpan ` U ) ` { X } ) ) = V )
46 4 5 40 41 42 43 44 14 14 45 8 9 6 lshpsmreu 
 |-  ( ph -> E! k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) )
47 oveq1 
 |-  ( k = .1. -> ( k .x. X ) = ( .1. .x. X ) )
48 47 oveq2d 
 |-  ( k = .1. -> ( w .+ ( k .x. X ) ) = ( w .+ ( .1. .x. X ) ) )
49 48 eqeq2d 
 |-  ( k = .1. -> ( X = ( w .+ ( k .x. X ) ) <-> X = ( w .+ ( .1. .x. X ) ) ) )
50 49 rexbidv 
 |-  ( k = .1. -> ( E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) <-> E. w e. ( ._|_ ` { X } ) X = ( w .+ ( .1. .x. X ) ) ) )
51 50 riota2 
 |-  ( ( .1. e. R /\ E! k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) -> ( E. w e. ( ._|_ ` { X } ) X = ( w .+ ( .1. .x. X ) ) <-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) = .1. ) )
52 39 46 51 syl2anc 
 |-  ( ph -> ( E. w e. ( ._|_ ` { X } ) X = ( w .+ ( .1. .x. X ) ) <-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) = .1. ) )
53 36 52 mpbid 
 |-  ( ph -> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) X = ( w .+ ( k .x. X ) ) ) = .1. )
54 20 53 eqtrd 
 |-  ( ph -> ( G ` X ) = .1. )