Metamath Proof Explorer

Theorem eqlkr2

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014)

Ref Expression
Hypotheses eqlkr.d 
|- D = ( Scalar ` W )
eqlkr.k 
|- K = ( Base ` D )
eqlkr.t 
|- .x. = ( .r ` D )
eqlkr.v 
|- V = ( Base ` W )
eqlkr.f 
|- F = ( LFnl ` W )
eqlkr.l 
|- L = ( LKer ` W )
Assertion eqlkr2 
|- ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K H = ( G oF .x. ( V X. { r } ) ) )

Proof

Step Hyp Ref Expression
1 eqlkr.d 
 |-  D = ( Scalar ` W )
2 eqlkr.k 
 |-  K = ( Base ` D )
3 eqlkr.t 
 |-  .x. = ( .r ` D )
4 eqlkr.v 
 |-  V = ( Base ` W )
5 eqlkr.f 
 |-  F = ( LFnl ` W )
6 eqlkr.l 
 |-  L = ( LKer ` W )
7 1 2 3 4 5 6 eqlkr 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
8 4 fvexi 
 |-  V e. _V
9 8 a1i 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> V e. _V )
10 simpl1 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> W e. LVec )
11 simpl2l 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> G e. F )
12 1 2 4 5 lflf 
 |-  ( ( W e. LVec /\ G e. F ) -> G : V --> K )
13 10 11 12 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> G : V --> K )
14 13 ffnd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> G Fn V )
15 vex 
 |-  r e. _V
16 fnconstg 
 |-  ( r e. _V -> ( V X. { r } ) Fn V )
17 15 16 mp1i 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> ( V X. { r } ) Fn V )
18 simpl2r 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> H e. F )
19 1 2 4 5 lflf 
 |-  ( ( W e. LVec /\ H e. F ) -> H : V --> K )
20 10 18 19 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> H : V --> K )
21 20 ffnd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> H Fn V )
22 eqidd 
 |-  ( ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) /\ x e. V ) -> ( G ` x ) = ( G ` x ) )
23 15 fvconst2 
 |-  ( x e. V -> ( ( V X. { r } ) ` x ) = r )
24 23 adantl 
 |-  ( ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) /\ x e. V ) -> ( ( V X. { r } ) ` x ) = r )
25 9 14 17 21 22 24 offveqb 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ r e. K ) -> ( H = ( G oF .x. ( V X. { r } ) ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) ) )
26 25 rexbidva 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> ( E. r e. K H = ( G oF .x. ( V X. { r } ) ) <-> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) ) )
27 7 26 mpbird 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> E. r e. K H = ( G oF .x. ( V X. { r } ) ) )