Metamath Proof Explorer


Theorem frlmvplusgvalc

Description: Coordinates of a sum with respect to a basis in a free module. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses frlmvplusgvalc.f
|- F = ( R freeLMod I )
frlmvplusgvalc.b
|- B = ( Base ` F )
frlmvplusgvalc.r
|- ( ph -> R e. V )
frlmvplusgvalc.i
|- ( ph -> I e. W )
frlmvplusgvalc.x
|- ( ph -> X e. B )
frlmvplusgvalc.y
|- ( ph -> Y e. B )
frlmvplusgvalc.j
|- ( ph -> J e. I )
frlmvplusgvalc.a
|- .+ = ( +g ` R )
frlmvplusgvalc.p
|- .+b = ( +g ` F )
Assertion frlmvplusgvalc
|- ( ph -> ( ( X .+b Y ) ` J ) = ( ( X ` J ) .+ ( Y ` J ) ) )

Proof

Step Hyp Ref Expression
1 frlmvplusgvalc.f
 |-  F = ( R freeLMod I )
2 frlmvplusgvalc.b
 |-  B = ( Base ` F )
3 frlmvplusgvalc.r
 |-  ( ph -> R e. V )
4 frlmvplusgvalc.i
 |-  ( ph -> I e. W )
5 frlmvplusgvalc.x
 |-  ( ph -> X e. B )
6 frlmvplusgvalc.y
 |-  ( ph -> Y e. B )
7 frlmvplusgvalc.j
 |-  ( ph -> J e. I )
8 frlmvplusgvalc.a
 |-  .+ = ( +g ` R )
9 frlmvplusgvalc.p
 |-  .+b = ( +g ` F )
10 1 2 3 4 5 6 8 9 frlmplusgval
 |-  ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
11 10 fveq1d
 |-  ( ph -> ( ( X .+b Y ) ` J ) = ( ( X oF .+ Y ) ` J ) )
12 eqid
 |-  ( Base ` R ) = ( Base ` R )
13 1 12 2 frlmbasmap
 |-  ( ( I e. W /\ X e. B ) -> X e. ( ( Base ` R ) ^m I ) )
14 4 5 13 syl2anc
 |-  ( ph -> X e. ( ( Base ` R ) ^m I ) )
15 fvexd
 |-  ( ph -> ( Base ` R ) e. _V )
16 15 4 elmapd
 |-  ( ph -> ( X e. ( ( Base ` R ) ^m I ) <-> X : I --> ( Base ` R ) ) )
17 14 16 mpbid
 |-  ( ph -> X : I --> ( Base ` R ) )
18 17 ffnd
 |-  ( ph -> X Fn I )
19 1 12 2 frlmbasmap
 |-  ( ( I e. W /\ Y e. B ) -> Y e. ( ( Base ` R ) ^m I ) )
20 4 6 19 syl2anc
 |-  ( ph -> Y e. ( ( Base ` R ) ^m I ) )
21 15 4 elmapd
 |-  ( ph -> ( Y e. ( ( Base ` R ) ^m I ) <-> Y : I --> ( Base ` R ) ) )
22 20 21 mpbid
 |-  ( ph -> Y : I --> ( Base ` R ) )
23 22 ffnd
 |-  ( ph -> Y Fn I )
24 fnfvof
 |-  ( ( ( X Fn I /\ Y Fn I ) /\ ( I e. W /\ J e. I ) ) -> ( ( X oF .+ Y ) ` J ) = ( ( X ` J ) .+ ( Y ` J ) ) )
25 18 23 4 7 24 syl22anc
 |-  ( ph -> ( ( X oF .+ Y ) ` J ) = ( ( X ` J ) .+ ( Y ` J ) ) )
26 11 25 eqtrd
 |-  ( ph -> ( ( X .+b Y ) ` J ) = ( ( X ` J ) .+ ( Y ` J ) ) )