Metamath Proof Explorer

Theorem lcfl7lem

Description: Lemma for lcfl7N . If two functionals G and J are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015)

Ref Expression
Hypotheses lcfl7lem.h 
|- H = ( LHyp ` K )
lcfl7lem.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfl7lem.u 
|- U = ( ( DVecH ` K ) ` W )
lcfl7lem.v 
|- V = ( Base ` U )
lcfl7lem.a 
|- .+ = ( +g ` U )
lcfl7lem.t 
|- .x. = ( .s ` U )
lcfl7lem.s 
|- S = ( Scalar ` U )
lcfl7lem.r 
|- R = ( Base ` S )
lcfl7lem.z 
|- .0. = ( 0g ` U )
lcfl7lem.f 
|- F = ( LFnl ` U )
lcfl7lem.l 
|- L = ( LKer ` U )
lcfl7lem.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfl7lem.g 
|- G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
lcfl7lem.j 
|- J = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { Y } ) v = ( w .+ ( k .x. Y ) ) ) )
lcfl7lem.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lcfl7lem.x2 
|- ( ph -> Y e. ( V \ { .0. } ) )
lcfl7lem.gj 
|- ( ph -> G = J )
Assertion lcfl7lem 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 lcfl7lem.h 
 |-  H = ( LHyp ` K )
2 lcfl7lem.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl7lem.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl7lem.v 
 |-  V = ( Base ` U )
5 lcfl7lem.a 
 |-  .+ = ( +g ` U )
6 lcfl7lem.t 
 |-  .x. = ( .s ` U )
7 lcfl7lem.s 
 |-  S = ( Scalar ` U )
8 lcfl7lem.r 
 |-  R = ( Base ` S )
9 lcfl7lem.z 
 |-  .0. = ( 0g ` U )
10 lcfl7lem.f 
 |-  F = ( LFnl ` U )
11 lcfl7lem.l 
 |-  L = ( LKer ` U )
12 lcfl7lem.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 lcfl7lem.g 
 |-  G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { X } ) v = ( w .+ ( k .x. X ) ) ) )
14 lcfl7lem.j 
 |-  J = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { Y } ) v = ( w .+ ( k .x. Y ) ) ) )
15 lcfl7lem.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
16 lcfl7lem.x2 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
17 lcfl7lem.gj 
 |-  ( ph -> G = J )
18 1 2 3 4 9 5 6 11 7 8 13 12 15 dochsnkr2cl 
 |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
19 18 eldifad 
 |-  ( ph -> X e. ( ._|_ ` ( L ` G ) ) )
20 17 fveq2d 
 |-  ( ph -> ( L ` G ) = ( L ` J ) )
21 1 2 3 4 9 5 6 11 7 8 14 12 16 dochsnkr2 
 |-  ( ph -> ( L ` J ) = ( ._|_ ` { Y } ) )
22 20 21 eqtrd 
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
23 22 fveq2d 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` { Y } ) ) )
24 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
25 16 eldifad 
 |-  ( ph -> Y e. V )
26 25 snssd 
 |-  ( ph -> { Y } C_ V )
27 1 3 2 4 24 12 26 dochocsp 
 |-  ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { Y } ) ) = ( ._|_ ` { Y } ) )
28 27 fveq2d 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { Y } ) ) ) = ( ._|_ ` ( ._|_ ` { Y } ) ) )
29 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
30 1 3 4 24 29 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( ( LSpan ` U ) ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
31 12 25 30 syl2anc 
 |-  ( ph -> ( ( LSpan ` U ) ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
32 1 29 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( LSpan ` U ) ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { Y } ) ) ) = ( ( LSpan ` U ) ` { Y } ) )
33 12 31 32 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { Y } ) ) ) = ( ( LSpan ` U ) ` { Y } ) )
34 23 28 33 3eqtr2d 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { Y } ) )
35 19 34 eleqtrd 
 |-  ( ph -> X e. ( ( LSpan ` U ) ` { Y } ) )
36 1 3 12 dvhlmod 
 |-  ( ph -> U e. LMod )
37 7 8 4 6 24 lspsnel 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( X e. ( ( LSpan ` U ) ` { Y } ) <-> E. s e. R X = ( s .x. Y ) ) )
38 36 25 37 syl2anc 
 |-  ( ph -> ( X e. ( ( LSpan ` U ) ` { Y } ) <-> E. s e. R X = ( s .x. Y ) ) )
39 35 38 mpbid 
 |-  ( ph -> E. s e. R X = ( s .x. Y ) )
40 simp3 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> X = ( s .x. Y ) )
41 fveq2 
 |-  ( X = ( s .x. Y ) -> ( G ` X ) = ( G ` ( s .x. Y ) ) )
42 41 3ad2ant3 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( G ` X ) = ( G ` ( s .x. Y ) ) )
43 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
44 1 2 3 4 5 6 9 7 8 43 12 16 14 dochfl1 
 |-  ( ph -> ( J ` Y ) = ( 1r ` S ) )
45 17 fveq1d 
 |-  ( ph -> ( G ` Y ) = ( J ` Y ) )
46 1 2 3 4 5 6 9 7 8 43 12 15 13 dochfl1 
 |-  ( ph -> ( G ` X ) = ( 1r ` S ) )
47 44 45 46 3eqtr4rd 
 |-  ( ph -> ( G ` X ) = ( G ` Y ) )
48 47 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( G ` X ) = ( G ` Y ) )
49 36 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> U e. LMod )
50 1 2 3 4 9 5 6 10 7 8 13 12 15 dochflcl 
 |-  ( ph -> G e. F )
51 50 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> G e. F )
52 simp2 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> s e. R )
53 25 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> Y e. V )
54 eqid 
 |-  ( .r ` S ) = ( .r ` S )
55 7 8 54 4 6 10 lflmul 
 |-  ( ( U e. LMod /\ G e. F /\ ( s e. R /\ Y e. V ) ) -> ( G ` ( s .x. Y ) ) = ( s ( .r ` S ) ( G ` Y ) ) )
56 49 51 52 53 55 syl112anc 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( G ` ( s .x. Y ) ) = ( s ( .r ` S ) ( G ` Y ) ) )
57 42 48 56 3eqtr3d 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( G ` Y ) = ( s ( .r ` S ) ( G ` Y ) ) )
58 57 oveq1d 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( ( s ( .r ` S ) ( G ` Y ) ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) )
59 7 lmodring 
 |-  ( U e. LMod -> S e. Ring )
60 36 59 syl 
 |-  ( ph -> S e. Ring )
61 60 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> S e. Ring )
62 7 8 4 10 lflcl 
 |-  ( ( U e. LMod /\ G e. F /\ Y e. V ) -> ( G ` Y ) e. R )
63 36 50 25 62 syl3anc 
 |-  ( ph -> ( G ` Y ) e. R )
64 63 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( G ` Y ) e. R )
65 1 3 12 dvhlvec 
 |-  ( ph -> U e. LVec )
66 7 lvecdrng 
 |-  ( U e. LVec -> S e. DivRing )
67 65 66 syl 
 |-  ( ph -> S e. DivRing )
68 45 44 eqtrd 
 |-  ( ph -> ( G ` Y ) = ( 1r ` S ) )
69 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
70 69 43 drngunz 
 |-  ( S e. DivRing -> ( 1r ` S ) =/= ( 0g ` S ) )
71 67 70 syl 
 |-  ( ph -> ( 1r ` S ) =/= ( 0g ` S ) )
72 68 71 eqnetrd 
 |-  ( ph -> ( G ` Y ) =/= ( 0g ` S ) )
73 eqid 
 |-  ( invr ` S ) = ( invr ` S )
74 8 69 73 drnginvrcl 
 |-  ( ( S e. DivRing /\ ( G ` Y ) e. R /\ ( G ` Y ) =/= ( 0g ` S ) ) -> ( ( invr ` S ) ` ( G ` Y ) ) e. R )
75 67 63 72 74 syl3anc 
 |-  ( ph -> ( ( invr ` S ) ` ( G ` Y ) ) e. R )
76 75 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( ( invr ` S ) ` ( G ` Y ) ) e. R )
77 8 54 ringass 
 |-  ( ( S e. Ring /\ ( s e. R /\ ( G ` Y ) e. R /\ ( ( invr ` S ) ` ( G ` Y ) ) e. R ) ) -> ( ( s ( .r ` S ) ( G ` Y ) ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( s ( .r ` S ) ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) ) )
78 61 52 64 76 77 syl13anc 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( ( s ( .r ` S ) ( G ` Y ) ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( s ( .r ` S ) ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) ) )
79 8 69 54 43 73 drnginvrr 
 |-  ( ( S e. DivRing /\ ( G ` Y ) e. R /\ ( G ` Y ) =/= ( 0g ` S ) ) -> ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( 1r ` S ) )
80 67 63 72 79 syl3anc 
 |-  ( ph -> ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( 1r ` S ) )
81 80 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) = ( 1r ` S ) )
82 81 oveq2d 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( s ( .r ` S ) ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) ) = ( s ( .r ` S ) ( 1r ` S ) ) )
83 58 78 82 3eqtrrd 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( s ( .r ` S ) ( 1r ` S ) ) = ( ( G ` Y ) ( .r ` S ) ( ( invr ` S ) ` ( G ` Y ) ) ) )
84 8 54 43 ringridm 
 |-  ( ( S e. Ring /\ s e. R ) -> ( s ( .r ` S ) ( 1r ` S ) ) = s )
85 61 52 84 syl2anc 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( s ( .r ` S ) ( 1r ` S ) ) = s )
86 83 85 81 3eqtr3d 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> s = ( 1r ` S ) )
87 oveq1 
 |-  ( s = ( 1r ` S ) -> ( s .x. Y ) = ( ( 1r ` S ) .x. Y ) )
88 4 7 6 43 lmodvs1 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( ( 1r ` S ) .x. Y ) = Y )
89 36 25 88 syl2anc 
 |-  ( ph -> ( ( 1r ` S ) .x. Y ) = Y )
90 89 3ad2ant1 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( ( 1r ` S ) .x. Y ) = Y )
91 87 90 sylan9eqr 
 |-  ( ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) /\ s = ( 1r ` S ) ) -> ( s .x. Y ) = Y )
92 86 91 mpdan 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> ( s .x. Y ) = Y )
93 40 92 eqtrd 
 |-  ( ( ph /\ s e. R /\ X = ( s .x. Y ) ) -> X = Y )
94 93 rexlimdv3a 
 |-  ( ph -> ( E. s e. R X = ( s .x. Y ) -> X = Y ) )
95 39 94 mpd 
 |-  ( ph -> X = Y )