Step |
Hyp |
Ref |
Expression |
1 |
|
lfladdcl.r |
|- R = ( Scalar ` W ) |
2 |
|
lfladdcl.p |
|- .+ = ( +g ` R ) |
3 |
|
lfladdcl.f |
|- F = ( LFnl ` W ) |
4 |
|
lfladdcl.w |
|- ( ph -> W e. LMod ) |
5 |
|
lfladdcl.g |
|- ( ph -> G e. F ) |
6 |
|
lfladdcl.h |
|- ( ph -> H e. F ) |
7 |
|
lfladdass.i |
|- ( ph -> I e. F ) |
8 |
|
fvexd |
|- ( ph -> ( Base ` W ) e. _V ) |
9 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
10 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
11 |
1 9 10 3
|
lflf |
|- ( ( W e. LMod /\ G e. F ) -> G : ( Base ` W ) --> ( Base ` R ) ) |
12 |
4 5 11
|
syl2anc |
|- ( ph -> G : ( Base ` W ) --> ( Base ` R ) ) |
13 |
1 9 10 3
|
lflf |
|- ( ( W e. LMod /\ H e. F ) -> H : ( Base ` W ) --> ( Base ` R ) ) |
14 |
4 6 13
|
syl2anc |
|- ( ph -> H : ( Base ` W ) --> ( Base ` R ) ) |
15 |
1 9 10 3
|
lflf |
|- ( ( W e. LMod /\ I e. F ) -> I : ( Base ` W ) --> ( Base ` R ) ) |
16 |
4 7 15
|
syl2anc |
|- ( ph -> I : ( Base ` W ) --> ( Base ` R ) ) |
17 |
1
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
18 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
19 |
4 17 18
|
3syl |
|- ( ph -> R e. Grp ) |
20 |
9 2
|
grpass |
|- ( ( R e. Grp /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) |
21 |
19 20
|
sylan |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) |
22 |
8 12 14 16 21
|
caofass |
|- ( ph -> ( ( G oF .+ H ) oF .+ I ) = ( G oF .+ ( H oF .+ I ) ) ) |