Metamath Proof Explorer

Theorem eqlkr4

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses eqlkr4.s 
|- S = ( Scalar ` W )
eqlkr4.r 
|- R = ( Base ` S )
eqlkr4.f 
|- F = ( LFnl ` W )
eqlkr4.k 
|- K = ( LKer ` W )
eqlkr4.d 
|- D = ( LDual ` W )
eqlkr4.t 
|- .x. = ( .s ` D )
eqlkr4.w 
|- ( ph -> W e. LVec )
eqlkr4.g 
|- ( ph -> G e. F )
eqlkr4.h 
|- ( ph -> H e. F )
eqlkr4.e 
|- ( ph -> ( K ` G ) = ( K ` H ) )
Assertion eqlkr4 
|- ( ph -> E. r e. R H = ( r .x. G ) )

Proof

Step Hyp Ref Expression
1 eqlkr4.s 
 |-  S = ( Scalar ` W )
2 eqlkr4.r 
 |-  R = ( Base ` S )
3 eqlkr4.f 
 |-  F = ( LFnl ` W )
4 eqlkr4.k 
 |-  K = ( LKer ` W )
5 eqlkr4.d 
 |-  D = ( LDual ` W )
6 eqlkr4.t 
 |-  .x. = ( .s ` D )
7 eqlkr4.w 
 |-  ( ph -> W e. LVec )
8 eqlkr4.g 
 |-  ( ph -> G e. F )
9 eqlkr4.h 
 |-  ( ph -> H e. F )
10 eqlkr4.e 
 |-  ( ph -> ( K ` G ) = ( K ` H ) )
11 eqid 
 |-  ( .r ` S ) = ( .r ` S )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 1 2 11 12 3 4 eqlkr2 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( K ` G ) = ( K ` H ) ) -> E. r e. R H = ( G oF ( .r ` S ) ( ( Base ` W ) X. { r } ) ) )
14 7 8 9 10 13 syl121anc 
 |-  ( ph -> E. r e. R H = ( G oF ( .r ` S ) ( ( Base ` W ) X. { r } ) ) )
15 7 adantr 
 |-  ( ( ph /\ r e. R ) -> W e. LVec )
16 simpr 
 |-  ( ( ph /\ r e. R ) -> r e. R )
17 8 adantr 
 |-  ( ( ph /\ r e. R ) -> G e. F )
18 3 12 1 2 11 5 6 15 16 17 ldualvs 
 |-  ( ( ph /\ r e. R ) -> ( r .x. G ) = ( G oF ( .r ` S ) ( ( Base ` W ) X. { r } ) ) )
19 18 eqeq2d 
 |-  ( ( ph /\ r e. R ) -> ( H = ( r .x. G ) <-> H = ( G oF ( .r ` S ) ( ( Base ` W ) X. { r } ) ) ) )
20 19 rexbidva 
 |-  ( ph -> ( E. r e. R H = ( r .x. G ) <-> E. r e. R H = ( G oF ( .r ` S ) ( ( Base ` W ) X. { r } ) ) ) )
21 14 20 mpbird 
 |-  ( ph -> E. r e. R H = ( r .x. G ) )