| 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 |
|
fvexd |
|- ( ph -> ( Base ` W ) e. _V ) |
| 8 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 9 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 10 |
1 8 9 3
|
lflf |
|- ( ( W e. LMod /\ G e. F ) -> G : ( Base ` W ) --> ( Base ` R ) ) |
| 11 |
4 5 10
|
syl2anc |
|- ( ph -> G : ( Base ` W ) --> ( Base ` R ) ) |
| 12 |
1 8 9 3
|
lflf |
|- ( ( W e. LMod /\ H e. F ) -> H : ( Base ` W ) --> ( Base ` R ) ) |
| 13 |
4 6 12
|
syl2anc |
|- ( ph -> H : ( Base ` W ) --> ( Base ` R ) ) |
| 14 |
1
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
| 15 |
|
ringabl |
|- ( R e. Ring -> R e. Abel ) |
| 16 |
4 14 15
|
3syl |
|- ( ph -> R e. Abel ) |
| 17 |
16
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> R e. Abel ) |
| 18 |
|
simprl |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> x e. ( Base ` R ) ) |
| 19 |
|
simprr |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> y e. ( Base ` R ) ) |
| 20 |
8 2
|
ablcom |
|- ( ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) = ( y .+ x ) ) |
| 21 |
17 18 19 20
|
syl3anc |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x .+ y ) = ( y .+ x ) ) |
| 22 |
7 11 13 21
|
caofcom |
|- ( ph -> ( G oF .+ H ) = ( H oF .+ G ) ) |