Step |
Hyp |
Ref |
Expression |
1 |
|
lflmul.d |
|- D = ( Scalar ` W ) |
2 |
|
lflmul.k |
|- K = ( Base ` D ) |
3 |
|
lflmul.t |
|- .X. = ( .r ` D ) |
4 |
|
lflmul.v |
|- V = ( Base ` W ) |
5 |
|
lflmul.s |
|- .x. = ( .s ` W ) |
6 |
|
lflmul.f |
|- F = ( LFnl ` W ) |
7 |
|
simp1 |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> W e. LMod ) |
8 |
|
simp2 |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> G e. F ) |
9 |
|
simp3l |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> R e. K ) |
10 |
|
simp3r |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> X e. V ) |
11 |
|
eqid |
|- ( 0g ` W ) = ( 0g ` W ) |
12 |
4 11
|
lmod0vcl |
|- ( W e. LMod -> ( 0g ` W ) e. V ) |
13 |
12
|
3ad2ant1 |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( 0g ` W ) e. V ) |
14 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
15 |
|
eqid |
|- ( +g ` D ) = ( +g ` D ) |
16 |
4 14 1 5 2 15 3 6
|
lfli |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V /\ ( 0g ` W ) e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) ) |
17 |
7 8 9 10 13 16
|
syl113anc |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) ) |
18 |
4 1 5 2
|
lmodvscl |
|- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V ) |
19 |
7 9 10 18
|
syl3anc |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( R .x. X ) e. V ) |
20 |
4 14 11
|
lmod0vrid |
|- ( ( W e. LMod /\ ( R .x. X ) e. V ) -> ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( R .x. X ) ) |
21 |
7 19 20
|
syl2anc |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( R .x. X ) ) |
22 |
21
|
fveq2d |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( ( R .x. X ) ( +g ` W ) ( 0g ` W ) ) ) = ( G ` ( R .x. X ) ) ) |
23 |
|
eqid |
|- ( 0g ` D ) = ( 0g ` D ) |
24 |
1 23 11 6
|
lfl0 |
|- ( ( W e. LMod /\ G e. F ) -> ( G ` ( 0g ` W ) ) = ( 0g ` D ) ) |
25 |
24
|
3adant3 |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( 0g ` W ) ) = ( 0g ` D ) ) |
26 |
25
|
oveq2d |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) = ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) ) |
27 |
1
|
lmodfgrp |
|- ( W e. LMod -> D e. Grp ) |
28 |
27
|
3ad2ant1 |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> D e. Grp ) |
29 |
1 2 4 6
|
lflcl |
|- ( ( W e. LMod /\ G e. F /\ X e. V ) -> ( G ` X ) e. K ) |
30 |
29
|
3adant3l |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` X ) e. K ) |
31 |
1 2 3
|
lmodmcl |
|- ( ( W e. LMod /\ R e. K /\ ( G ` X ) e. K ) -> ( R .X. ( G ` X ) ) e. K ) |
32 |
7 9 30 31
|
syl3anc |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( R .X. ( G ` X ) ) e. K ) |
33 |
2 15 23
|
grprid |
|- ( ( D e. Grp /\ ( R .X. ( G ` X ) ) e. K ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) = ( R .X. ( G ` X ) ) ) |
34 |
28 32 33
|
syl2anc |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( 0g ` D ) ) = ( R .X. ( G ` X ) ) ) |
35 |
26 34
|
eqtrd |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( ( R .X. ( G ` X ) ) ( +g ` D ) ( G ` ( 0g ` W ) ) ) = ( R .X. ( G ` X ) ) ) |
36 |
17 22 35
|
3eqtr3d |
|- ( ( W e. LMod /\ G e. F /\ ( R e. K /\ X e. V ) ) -> ( G ` ( R .x. X ) ) = ( R .X. ( G ` X ) ) ) |