Step |
Hyp |
Ref |
Expression |
1 |
|
frlmval.f |
|- F = ( R freeLMod I ) |
2 |
|
elex |
|- ( R e. V -> R e. _V ) |
3 |
|
elex |
|- ( I e. W -> I e. _V ) |
4 |
|
id |
|- ( r = R -> r = R ) |
5 |
|
fveq2 |
|- ( r = R -> ( ringLMod ` r ) = ( ringLMod ` R ) ) |
6 |
5
|
sneqd |
|- ( r = R -> { ( ringLMod ` r ) } = { ( ringLMod ` R ) } ) |
7 |
6
|
xpeq2d |
|- ( r = R -> ( i X. { ( ringLMod ` r ) } ) = ( i X. { ( ringLMod ` R ) } ) ) |
8 |
4 7
|
oveq12d |
|- ( r = R -> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) = ( R (+)m ( i X. { ( ringLMod ` R ) } ) ) ) |
9 |
|
xpeq1 |
|- ( i = I -> ( i X. { ( ringLMod ` R ) } ) = ( I X. { ( ringLMod ` R ) } ) ) |
10 |
9
|
oveq2d |
|- ( i = I -> ( R (+)m ( i X. { ( ringLMod ` R ) } ) ) = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) |
11 |
|
df-frlm |
|- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) ) |
12 |
|
ovex |
|- ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) e. _V |
13 |
8 10 11 12
|
ovmpo |
|- ( ( R e. _V /\ I e. _V ) -> ( R freeLMod I ) = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) |
14 |
2 3 13
|
syl2an |
|- ( ( R e. V /\ I e. W ) -> ( R freeLMod I ) = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) |
15 |
1 14
|
syl5eq |
|- ( ( R e. V /\ I e. W ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) |