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 ) ) )