Metamath Proof Explorer

Theorem eqlkr

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-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 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 ) )

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 simpl1 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> W e. LVec )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 1 lmodring 
 |-  ( W e. LMod -> D e. Ring )
10 8 9 syl 
 |-  ( W e. LVec -> D e. Ring )
11 7 10 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> D e. Ring )
12 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
13 2 12 ringidcl 
 |-  ( D e. Ring -> ( 1r ` D ) e. K )
14 11 13 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( 1r ` D ) e. K )
15 simp11 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> W e. LVec )
16 15 10 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> D e. Ring )
17 simp12l 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> G e. F )
18 simp3 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> x e. V )
19 1 2 4 5 lflcl 
 |-  ( ( W e. LVec /\ G e. F /\ x e. V ) -> ( G ` x ) e. K )
20 15 17 18 19 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( G ` x ) e. K )
21 2 3 12 ringridm 
 |-  ( ( D e. Ring /\ ( G ` x ) e. K ) -> ( ( G ` x ) .x. ( 1r ` D ) ) = ( G ` x ) )
22 16 20 21 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( ( G ` x ) .x. ( 1r ` D ) ) = ( G ` x ) )
23 simp2 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> G = ( V X. { ( 0g ` D ) } ) )
24 simp13 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( L ` G ) = ( L ` H ) )
25 15 8 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> W e. LMod )
26 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
27 1 26 4 5 6 lkr0f 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
28 25 17 27 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
29 23 28 mpbird 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( L ` G ) = V )
30 24 29 eqtr3d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( L ` H ) = V )
31 simp12r 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> H e. F )
32 1 26 4 5 6 lkr0f 
 |-  ( ( W e. LMod /\ H e. F ) -> ( ( L ` H ) = V <-> H = ( V X. { ( 0g ` D ) } ) ) )
33 25 31 32 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( ( L ` H ) = V <-> H = ( V X. { ( 0g ` D ) } ) ) )
34 30 33 mpbid 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> H = ( V X. { ( 0g ` D ) } ) )
35 23 34 eqtr4d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> G = H )
36 35 fveq1d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( G ` x ) = ( H ` x ) )
37 22 36 eqtr2d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) /\ x e. V ) -> ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) )
38 37 3expia 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( x e. V -> ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) ) )
39 38 ralrimiv 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) )
40 oveq2 
 |-  ( r = ( 1r ` D ) -> ( ( G ` x ) .x. r ) = ( ( G ` x ) .x. ( 1r ` D ) ) )
41 40 eqeq2d 
 |-  ( r = ( 1r ` D ) -> ( ( H ` x ) = ( ( G ` x ) .x. r ) <-> ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) ) )
42 41 ralbidv 
 |-  ( r = ( 1r ` D ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) ) )
43 42 rspcev 
 |-  ( ( ( 1r ` D ) e. K /\ A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( 1r ` D ) ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
44 14 39 43 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
45 simpl1 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> W e. LVec )
46 simpl2l 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> G e. F )
47 simpr 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> G =/= ( V X. { ( 0g ` D ) } ) )
48 1 26 12 4 5 lfl1 
 |-  ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> E. z e. V ( G ` z ) = ( 1r ` D ) )
49 45 46 47 48 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> E. z e. V ( G ` z ) = ( 1r ` D ) )
50 simpl1 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> W e. LVec )
51 simpl2r 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> H e. F )
52 simpr2 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> z e. V )
53 1 2 4 5 lflcl 
 |-  ( ( W e. LVec /\ H e. F /\ z e. V ) -> ( H ` z ) e. K )
54 50 51 52 53 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> ( H ` z ) e. K )
55 simp11 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> W e. LVec )
56 55 8 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> W e. LMod )
57 simp12r 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> H e. F )
58 simp12l 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> G e. F )
59 simp3 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> x e. V )
60 1 2 4 5 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ x e. V ) -> ( G ` x ) e. K )
61 56 58 59 60 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` x ) e. K )
62 simp22 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> z e. V )
63 eqid 
 |-  ( .s ` W ) = ( .s ` W )
64 1 2 3 4 63 5 lflmul 
 |-  ( ( W e. LMod /\ H e. F /\ ( ( G ` x ) e. K /\ z e. V ) ) -> ( H ` ( ( G ` x ) ( .s ` W ) z ) ) = ( ( G ` x ) .x. ( H ` z ) ) )
65 56 57 61 62 64 syl112anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` ( ( G ` x ) ( .s ` W ) z ) ) = ( ( G ` x ) .x. ( H ` z ) ) )
66 65 oveq2d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( H ` x ) ( -g ` D ) ( H ` ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( H ` x ) ( -g ` D ) ( ( G ` x ) .x. ( H ` z ) ) ) )
67 4 1 63 2 lmodvscl 
 |-  ( ( W e. LMod /\ ( G ` x ) e. K /\ z e. V ) -> ( ( G ` x ) ( .s ` W ) z ) e. V )
68 56 61 62 67 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) ( .s ` W ) z ) e. V )
69 eqid 
 |-  ( -g ` D ) = ( -g ` D )
70 eqid 
 |-  ( -g ` W ) = ( -g ` W )
71 1 69 4 70 5 lflsub 
 |-  ( ( W e. LMod /\ H e. F /\ ( x e. V /\ ( ( G ` x ) ( .s ` W ) z ) e. V ) ) -> ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( H ` x ) ( -g ` D ) ( H ` ( ( G ` x ) ( .s ` W ) z ) ) ) )
72 56 57 59 68 71 syl112anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( H ` x ) ( -g ` D ) ( H ` ( ( G ` x ) ( .s ` W ) z ) ) ) )
73 4 70 lmodvsubcl 
 |-  ( ( W e. LMod /\ x e. V /\ ( ( G ` x ) ( .s ` W ) z ) e. V ) -> ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V )
74 56 59 68 73 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V )
75 1 69 4 70 5 lflsub 
 |-  ( ( W e. LMod /\ G e. F /\ ( x e. V /\ ( ( G ` x ) ( .s ` W ) z ) e. V ) ) -> ( G ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( G ` x ) ( -g ` D ) ( G ` ( ( G ` x ) ( .s ` W ) z ) ) ) )
76 56 58 59 68 75 syl112anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( G ` x ) ( -g ` D ) ( G ` ( ( G ` x ) ( .s ` W ) z ) ) ) )
77 55 58 59 19 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` x ) e. K )
78 1 2 3 4 63 5 lflmul 
 |-  ( ( W e. LMod /\ G e. F /\ ( ( G ` x ) e. K /\ z e. V ) ) -> ( G ` ( ( G ` x ) ( .s ` W ) z ) ) = ( ( G ` x ) .x. ( G ` z ) ) )
79 56 58 77 62 78 syl112anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` ( ( G ` x ) ( .s ` W ) z ) ) = ( ( G ` x ) .x. ( G ` z ) ) )
80 simp23 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` z ) = ( 1r ` D ) )
81 80 oveq2d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) .x. ( G ` z ) ) = ( ( G ` x ) .x. ( 1r ` D ) ) )
82 55 10 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> D e. Ring )
83 82 77 21 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) .x. ( 1r ` D ) ) = ( G ` x ) )
84 79 81 83 3eqtrd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` ( ( G ` x ) ( .s ` W ) z ) ) = ( G ` x ) )
85 84 oveq2d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) ( -g ` D ) ( G ` ( ( G ` x ) ( .s ` W ) z ) ) ) = ( ( G ` x ) ( -g ` D ) ( G ` x ) ) )
86 1 lmodfgrp 
 |-  ( W e. LMod -> D e. Grp )
87 8 86 syl 
 |-  ( W e. LVec -> D e. Grp )
88 55 87 syl 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> D e. Grp )
89 2 26 69 grpsubid 
 |-  ( ( D e. Grp /\ ( G ` x ) e. K ) -> ( ( G ` x ) ( -g ` D ) ( G ` x ) ) = ( 0g ` D ) )
90 88 77 89 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) ( -g ` D ) ( G ` x ) ) = ( 0g ` D ) )
91 76 85 90 3eqtrd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( G ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) )
92 4 1 26 5 6 ellkr 
 |-  ( ( W e. LVec /\ G e. F ) -> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` G ) <-> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V /\ ( G ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) ) ) )
93 55 58 92 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` G ) <-> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V /\ ( G ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) ) ) )
94 74 91 93 mpbir2and 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` G ) )
95 simp13 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( L ` G ) = ( L ` H ) )
96 94 95 eleqtrd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` H ) )
97 4 1 26 5 6 ellkr 
 |-  ( ( W e. LVec /\ H e. F ) -> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` H ) <-> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V /\ ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) ) ) )
98 55 57 97 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. ( L ` H ) <-> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V /\ ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) ) ) )
99 96 98 mpbid 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) e. V /\ ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) ) )
100 99 simprd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` ( x ( -g ` W ) ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) )
101 72 100 eqtr3d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( H ` x ) ( -g ` D ) ( H ` ( ( G ` x ) ( .s ` W ) z ) ) ) = ( 0g ` D ) )
102 66 101 eqtr3d 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( H ` x ) ( -g ` D ) ( ( G ` x ) .x. ( H ` z ) ) ) = ( 0g ` D ) )
103 1 2 4 5 lflcl 
 |-  ( ( W e. LVec /\ H e. F /\ x e. V ) -> ( H ` x ) e. K )
104 55 57 59 103 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` x ) e. K )
105 54 3adant3 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` z ) e. K )
106 1 2 3 lmodmcl 
 |-  ( ( W e. LMod /\ ( G ` x ) e. K /\ ( H ` z ) e. K ) -> ( ( G ` x ) .x. ( H ` z ) ) e. K )
107 56 77 105 106 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( G ` x ) .x. ( H ` z ) ) e. K )
108 2 26 69 grpsubeq0 
 |-  ( ( D e. Grp /\ ( H ` x ) e. K /\ ( ( G ` x ) .x. ( H ` z ) ) e. K ) -> ( ( ( H ` x ) ( -g ` D ) ( ( G ` x ) .x. ( H ` z ) ) ) = ( 0g ` D ) <-> ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) )
109 88 104 107 108 syl3anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( ( ( H ` x ) ( -g ` D ) ( ( G ` x ) .x. ( H ` z ) ) ) = ( 0g ` D ) <-> ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) )
110 102 109 mpbid 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) /\ x e. V ) -> ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) )
111 110 3expia 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> ( x e. V -> ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) )
112 111 ralrimiv 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) )
113 oveq2 
 |-  ( r = ( H ` z ) -> ( ( G ` x ) .x. r ) = ( ( G ` x ) .x. ( H ` z ) ) )
114 113 eqeq2d 
 |-  ( r = ( H ` z ) -> ( ( H ` x ) = ( ( G ` x ) .x. r ) <-> ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) )
115 114 ralbidv 
 |-  ( r = ( H ` z ) -> ( A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) <-> A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) )
116 115 rspcev 
 |-  ( ( ( H ` z ) e. K /\ A. x e. V ( H ` x ) = ( ( G ` x ) .x. ( H ` z ) ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
117 54 112 116 syl2anc 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ ( G =/= ( V X. { ( 0g ` D ) } ) /\ z e. V /\ ( G ` z ) = ( 1r ` D ) ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
118 117 3exp2 
 |-  ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) -> ( G =/= ( V X. { ( 0g ` D ) } ) -> ( z e. V -> ( ( G ` z ) = ( 1r ` D ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) ) ) ) )
119 118 imp 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( z e. V -> ( ( G ` z ) = ( 1r ` D ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) ) ) )
120 119 rexlimdv 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( E. z e. V ( G ` z ) = ( 1r ` D ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) ) )
121 49 120 mpd 
 |-  ( ( ( W e. LVec /\ ( G e. F /\ H e. F ) /\ ( L ` G ) = ( L ` H ) ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> E. r e. K A. x e. V ( H ` x ) = ( ( G ` x ) .x. r ) )
122 44 121 pm2.61dane 
 |-  ( ( 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 ) )