Step |
Hyp |
Ref |
Expression |
1 |
|
frlmplusgvalb.f |
|- F = ( R freeLMod I ) |
2 |
|
frlmplusgvalb.b |
|- B = ( Base ` F ) |
3 |
|
frlmplusgvalb.i |
|- ( ph -> I e. W ) |
4 |
|
frlmplusgvalb.x |
|- ( ph -> X e. B ) |
5 |
|
frlmplusgvalb.z |
|- ( ph -> Z e. B ) |
6 |
|
frlmplusgvalb.r |
|- ( ph -> R e. Ring ) |
7 |
|
frlmvscavalb.k |
|- K = ( Base ` R ) |
8 |
|
frlmvscavalb.a |
|- ( ph -> A e. K ) |
9 |
|
frlmvscavalb.v |
|- .xb = ( .s ` F ) |
10 |
|
frlmvscavalb.t |
|- .x. = ( .r ` R ) |
11 |
|
frlmvplusgscavalb.y |
|- ( ph -> Y e. B ) |
12 |
|
frlmvplusgscavalb.a |
|- .+ = ( +g ` R ) |
13 |
|
frlmvplusgscavalb.p |
|- .+b = ( +g ` F ) |
14 |
|
frlmvplusgscavalb.c |
|- ( ph -> C e. K ) |
15 |
1
|
frlmlmod |
|- ( ( R e. Ring /\ I e. W ) -> F e. LMod ) |
16 |
6 3 15
|
syl2anc |
|- ( ph -> F e. LMod ) |
17 |
8 7
|
eleqtrdi |
|- ( ph -> A e. ( Base ` R ) ) |
18 |
1
|
frlmsca |
|- ( ( R e. Ring /\ I e. W ) -> R = ( Scalar ` F ) ) |
19 |
6 3 18
|
syl2anc |
|- ( ph -> R = ( Scalar ` F ) ) |
20 |
19
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) ) |
21 |
17 20
|
eleqtrd |
|- ( ph -> A e. ( Base ` ( Scalar ` F ) ) ) |
22 |
|
eqid |
|- ( Scalar ` F ) = ( Scalar ` F ) |
23 |
|
eqid |
|- ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) ) |
24 |
2 22 9 23
|
lmodvscl |
|- ( ( F e. LMod /\ A e. ( Base ` ( Scalar ` F ) ) /\ X e. B ) -> ( A .xb X ) e. B ) |
25 |
16 21 4 24
|
syl3anc |
|- ( ph -> ( A .xb X ) e. B ) |
26 |
14 7
|
eleqtrdi |
|- ( ph -> C e. ( Base ` R ) ) |
27 |
26 20
|
eleqtrd |
|- ( ph -> C e. ( Base ` ( Scalar ` F ) ) ) |
28 |
2 22 9 23
|
lmodvscl |
|- ( ( F e. LMod /\ C e. ( Base ` ( Scalar ` F ) ) /\ Y e. B ) -> ( C .xb Y ) e. B ) |
29 |
16 27 11 28
|
syl3anc |
|- ( ph -> ( C .xb Y ) e. B ) |
30 |
1 2 3 25 5 6 29 12 13
|
frlmplusgvalb |
|- ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) ) ) |
31 |
3
|
adantr |
|- ( ( ph /\ i e. I ) -> I e. W ) |
32 |
8
|
adantr |
|- ( ( ph /\ i e. I ) -> A e. K ) |
33 |
4
|
adantr |
|- ( ( ph /\ i e. I ) -> X e. B ) |
34 |
|
simpr |
|- ( ( ph /\ i e. I ) -> i e. I ) |
35 |
1 2 7 31 32 33 34 9 10
|
frlmvscaval |
|- ( ( ph /\ i e. I ) -> ( ( A .xb X ) ` i ) = ( A .x. ( X ` i ) ) ) |
36 |
14
|
adantr |
|- ( ( ph /\ i e. I ) -> C e. K ) |
37 |
11
|
adantr |
|- ( ( ph /\ i e. I ) -> Y e. B ) |
38 |
1 2 7 31 36 37 34 9 10
|
frlmvscaval |
|- ( ( ph /\ i e. I ) -> ( ( C .xb Y ) ` i ) = ( C .x. ( Y ` i ) ) ) |
39 |
35 38
|
oveq12d |
|- ( ( ph /\ i e. I ) -> ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) |
40 |
39
|
eqeq2d |
|- ( ( ph /\ i e. I ) -> ( ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) <-> ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) ) |
41 |
40
|
ralbidva |
|- ( ph -> ( A. i e. I ( Z ` i ) = ( ( ( A .xb X ) ` i ) .+ ( ( C .xb Y ) ` i ) ) <-> A. i e. I ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) ) |
42 |
30 41
|
bitrd |
|- ( ph -> ( Z = ( ( A .xb X ) .+b ( C .xb Y ) ) <-> A. i e. I ( Z ` i ) = ( ( A .x. ( X ` i ) ) .+ ( C .x. ( Y ` i ) ) ) ) ) |