Metamath Proof Explorer

Theorem eqlkr3

Description: Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses eqlkr3.v 
|- V = ( Base ` W )
eqlkr3.s 
|- S = ( Scalar ` W )
eqlkr3.r 
|- R = ( Base ` S )
eqlkr3.o 
|- .0. = ( 0g ` S )
eqlkr3.f 
|- F = ( LFnl ` W )
eqlkr3.k 
|- K = ( LKer ` W )
eqlkr3.w 
|- ( ph -> W e. LVec )
eqlkr3.x 
|- ( ph -> X e. V )
eqlkr3.g 
|- ( ph -> G e. F )
eqlkr3.h 
|- ( ph -> H e. F )
eqlkr3.e 
|- ( ph -> ( K ` G ) = ( K ` H ) )
eqlkr3.a 
|- ( ph -> ( G ` X ) = ( H ` X ) )
eqlkr3.n 
|- ( ph -> ( G ` X ) =/= .0. )
Assertion eqlkr3 
|- ( ph -> G = H )

Proof

Step Hyp Ref Expression
1 eqlkr3.v 
 |-  V = ( Base ` W )
2 eqlkr3.s 
 |-  S = ( Scalar ` W )
3 eqlkr3.r 
 |-  R = ( Base ` S )
4 eqlkr3.o 
 |-  .0. = ( 0g ` S )
5 eqlkr3.f 
 |-  F = ( LFnl ` W )
6 eqlkr3.k 
 |-  K = ( LKer ` W )
7 eqlkr3.w 
 |-  ( ph -> W e. LVec )
8 eqlkr3.x 
 |-  ( ph -> X e. V )
9 eqlkr3.g 
 |-  ( ph -> G e. F )
10 eqlkr3.h 
 |-  ( ph -> H e. F )
11 eqlkr3.e 
 |-  ( ph -> ( K ` G ) = ( K ` H ) )
12 eqlkr3.a 
 |-  ( ph -> ( G ` X ) = ( H ` X ) )
13 eqlkr3.n 
 |-  ( ph -> ( G ` X ) =/= .0. )
14 2 3 1 5 lflf 
 |-  ( ( W e. LVec /\ G e. F ) -> G : V --> R )
15 7 9 14 syl2anc 
 |-  ( ph -> G : V --> R )
16 15 ffnd 
 |-  ( ph -> G Fn V )
17 2 3 1 5 lflf 
 |-  ( ( W e. LVec /\ H e. F ) -> H : V --> R )
18 7 10 17 syl2anc 
 |-  ( ph -> H : V --> R )
19 18 ffnd 
 |-  ( ph -> H Fn V )
20 eqid 
 |-  ( .r ` S ) = ( .r ` S )
21 2 3 20 1 5 6 eqlkr 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( K ` G ) = ( K ` H ) ) -> E. r e. R A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) )
22 7 9 10 11 21 syl121anc 
 |-  ( ph -> E. r e. R A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) )
23 8 adantr 
 |-  ( ( ph /\ r e. R ) -> X e. V )
24 fveq2 
 |-  ( x = X -> ( H ` x ) = ( H ` X ) )
25 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
26 25 oveq1d 
 |-  ( x = X -> ( ( G ` x ) ( .r ` S ) r ) = ( ( G ` X ) ( .r ` S ) r ) )
27 24 26 eqeq12d 
 |-  ( x = X -> ( ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) <-> ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) )
28 27 rspcv 
 |-  ( X e. V -> ( A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) -> ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) )
29 23 28 syl 
 |-  ( ( ph /\ r e. R ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) -> ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) )
30 12 adantr 
 |-  ( ( ph /\ r e. R ) -> ( G ` X ) = ( H ` X ) )
31 30 adantr 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( G ` X ) = ( H ` X ) )
32 simpr 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) )
33 31 32 eqtr2d 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( ( G ` X ) ( .r ` S ) r ) = ( G ` X ) )
34 33 oveq2d 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( ( G ` X ) ( .r ` S ) r ) ) = ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) )
35 2 lvecdrng 
 |-  ( W e. LVec -> S e. DivRing )
36 7 35 syl 
 |-  ( ph -> S e. DivRing )
37 36 adantr 
 |-  ( ( ph /\ r e. R ) -> S e. DivRing )
38 2 3 1 5 lflcl 
 |-  ( ( W e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. R )
39 7 9 8 38 syl3anc 
 |-  ( ph -> ( G ` X ) e. R )
40 39 adantr 
 |-  ( ( ph /\ r e. R ) -> ( G ` X ) e. R )
41 13 adantr 
 |-  ( ( ph /\ r e. R ) -> ( G ` X ) =/= .0. )
42 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
43 eqid 
 |-  ( invr ` S ) = ( invr ` S )
44 3 4 20 42 43 drnginvrl 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. R /\ ( G ` X ) =/= .0. ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) = ( 1r ` S ) )
45 37 40 41 44 syl3anc 
 |-  ( ( ph /\ r e. R ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) = ( 1r ` S ) )
46 45 oveq1d 
 |-  ( ( ph /\ r e. R ) -> ( ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) ( .r ` S ) r ) = ( ( 1r ` S ) ( .r ` S ) r ) )
47 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
48 7 47 syl 
 |-  ( ph -> W e. LMod )
49 2 lmodring 
 |-  ( W e. LMod -> S e. Ring )
50 48 49 syl 
 |-  ( ph -> S e. Ring )
51 50 adantr 
 |-  ( ( ph /\ r e. R ) -> S e. Ring )
52 3 4 43 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( G ` X ) e. R /\ ( G ` X ) =/= .0. ) -> ( ( invr ` S ) ` ( G ` X ) ) e. R )
53 37 40 41 52 syl3anc 
 |-  ( ( ph /\ r e. R ) -> ( ( invr ` S ) ` ( G ` X ) ) e. R )
54 simpr 
 |-  ( ( ph /\ r e. R ) -> r e. R )
55 3 20 ringass 
 |-  ( ( S e. Ring /\ ( ( ( invr ` S ) ` ( G ` X ) ) e. R /\ ( G ` X ) e. R /\ r e. R ) ) -> ( ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) ( .r ` S ) r ) = ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( ( G ` X ) ( .r ` S ) r ) ) )
56 51 53 40 54 55 syl13anc 
 |-  ( ( ph /\ r e. R ) -> ( ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) ( .r ` S ) r ) = ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( ( G ` X ) ( .r ` S ) r ) ) )
57 3 20 42 ringlidm 
 |-  ( ( S e. Ring /\ r e. R ) -> ( ( 1r ` S ) ( .r ` S ) r ) = r )
58 51 54 57 syl2anc 
 |-  ( ( ph /\ r e. R ) -> ( ( 1r ` S ) ( .r ` S ) r ) = r )
59 46 56 58 3eqtr3d 
 |-  ( ( ph /\ r e. R ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( ( G ` X ) ( .r ` S ) r ) ) = r )
60 59 adantr 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( ( G ` X ) ( .r ` S ) r ) ) = r )
61 45 adantr 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> ( ( ( invr ` S ) ` ( G ` X ) ) ( .r ` S ) ( G ` X ) ) = ( 1r ` S ) )
62 34 60 61 3eqtr3d 
 |-  ( ( ( ph /\ r e. R ) /\ ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) ) -> r = ( 1r ` S ) )
63 62 ex 
 |-  ( ( ph /\ r e. R ) -> ( ( H ` X ) = ( ( G ` X ) ( .r ` S ) r ) -> r = ( 1r ` S ) ) )
64 29 63 syld 
 |-  ( ( ph /\ r e. R ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) -> r = ( 1r ` S ) ) )
65 64 ancrd 
 |-  ( ( ph /\ r e. R ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) -> ( r = ( 1r ` S ) /\ A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) ) ) )
66 65 reximdva 
 |-  ( ph -> ( E. r e. R A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) -> E. r e. R ( r = ( 1r ` S ) /\ A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) ) ) )
67 22 66 mpd 
 |-  ( ph -> E. r e. R ( r = ( 1r ` S ) /\ A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) ) )
68 3 42 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. R )
69 50 68 syl 
 |-  ( ph -> ( 1r ` S ) e. R )
70 oveq2 
 |-  ( r = ( 1r ` S ) -> ( ( G ` x ) ( .r ` S ) r ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) )
71 70 eqeq2d 
 |-  ( r = ( 1r ` S ) -> ( ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) <-> ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) ) )
72 71 ralbidv 
 |-  ( r = ( 1r ` S ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) ) )
73 72 ceqsrexv 
 |-  ( ( 1r ` S ) e. R -> ( E. r e. R ( r = ( 1r ` S ) /\ A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) ) )
74 69 73 syl 
 |-  ( ph -> ( E. r e. R ( r = ( 1r ` S ) /\ A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) r ) ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) ) )
75 67 74 mpbid 
 |-  ( ph -> A. x e. V ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) )
76 75 r19.21bi 
 |-  ( ( ph /\ x e. V ) -> ( H ` x ) = ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) )
77 48 adantr 
 |-  ( ( ph /\ x e. V ) -> W e. LMod )
78 77 49 syl 
 |-  ( ( ph /\ x e. V ) -> S e. Ring )
79 7 adantr 
 |-  ( ( ph /\ x e. V ) -> W e. LVec )
80 9 adantr 
 |-  ( ( ph /\ x e. V ) -> G e. F )
81 simpr 
 |-  ( ( ph /\ x e. V ) -> x e. V )
82 2 3 1 5 lflcl 
 |-  ( ( W e. LVec /\ G e. F /\ x e. V ) -> ( G ` x ) e. R )
83 79 80 81 82 syl3anc 
 |-  ( ( ph /\ x e. V ) -> ( G ` x ) e. R )
84 3 20 42 ringridm 
 |-  ( ( S e. Ring /\ ( G ` x ) e. R ) -> ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) = ( G ` x ) )
85 78 83 84 syl2anc 
 |-  ( ( ph /\ x e. V ) -> ( ( G ` x ) ( .r ` S ) ( 1r ` S ) ) = ( G ` x ) )
86 76 85 eqtr2d 
 |-  ( ( ph /\ x e. V ) -> ( G ` x ) = ( H ` x ) )
87 16 19 86 eqfnfvd 
 |-  ( ph -> G = H )