Metamath Proof Explorer


Theorem frlmvscaval

Description: Coordinates of a scalar multiple with respect to a basis in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses frlmvscaval.y โŠข ๐‘Œ = ( ๐‘… freeLMod ๐ผ )
frlmvscaval.b โŠข ๐ต = ( Base โ€˜ ๐‘Œ )
frlmvscaval.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
frlmvscaval.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘Š )
frlmvscaval.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐พ )
frlmvscaval.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
frlmvscaval.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ๐ผ )
frlmvscaval.v โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘Œ )
frlmvscaval.t โŠข ยท = ( .r โ€˜ ๐‘… )
Assertion frlmvscaval ( ๐œ‘ โ†’ ( ( ๐ด โˆ™ ๐‘‹ ) โ€˜ ๐ฝ ) = ( ๐ด ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) )

Proof

Step Hyp Ref Expression
1 frlmvscaval.y โŠข ๐‘Œ = ( ๐‘… freeLMod ๐ผ )
2 frlmvscaval.b โŠข ๐ต = ( Base โ€˜ ๐‘Œ )
3 frlmvscaval.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
4 frlmvscaval.i โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ๐‘Š )
5 frlmvscaval.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐พ )
6 frlmvscaval.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
7 frlmvscaval.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ๐ผ )
8 frlmvscaval.v โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘Œ )
9 frlmvscaval.t โŠข ยท = ( .r โ€˜ ๐‘… )
10 1 2 3 4 5 6 8 9 frlmvscafval โŠข ( ๐œ‘ โ†’ ( ๐ด โˆ™ ๐‘‹ ) = ( ( ๐ผ ร— { ๐ด } ) โˆ˜f ยท ๐‘‹ ) )
11 10 fveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐ด โˆ™ ๐‘‹ ) โ€˜ ๐ฝ ) = ( ( ( ๐ผ ร— { ๐ด } ) โˆ˜f ยท ๐‘‹ ) โ€˜ ๐ฝ ) )
12 fnconstg โŠข ( ๐ด โˆˆ ๐พ โ†’ ( ๐ผ ร— { ๐ด } ) Fn ๐ผ )
13 5 12 syl โŠข ( ๐œ‘ โ†’ ( ๐ผ ร— { ๐ด } ) Fn ๐ผ )
14 1 3 2 frlmbasf โŠข ( ( ๐ผ โˆˆ ๐‘Š โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘‹ : ๐ผ โŸถ ๐พ )
15 4 6 14 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘‹ : ๐ผ โŸถ ๐พ )
16 15 ffnd โŠข ( ๐œ‘ โ†’ ๐‘‹ Fn ๐ผ )
17 fnfvof โŠข ( ( ( ( ๐ผ ร— { ๐ด } ) Fn ๐ผ โˆง ๐‘‹ Fn ๐ผ ) โˆง ( ๐ผ โˆˆ ๐‘Š โˆง ๐ฝ โˆˆ ๐ผ ) ) โ†’ ( ( ( ๐ผ ร— { ๐ด } ) โˆ˜f ยท ๐‘‹ ) โ€˜ ๐ฝ ) = ( ( ( ๐ผ ร— { ๐ด } ) โ€˜ ๐ฝ ) ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) )
18 13 16 4 7 17 syl22anc โŠข ( ๐œ‘ โ†’ ( ( ( ๐ผ ร— { ๐ด } ) โˆ˜f ยท ๐‘‹ ) โ€˜ ๐ฝ ) = ( ( ( ๐ผ ร— { ๐ด } ) โ€˜ ๐ฝ ) ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) )
19 fvconst2g โŠข ( ( ๐ด โˆˆ ๐พ โˆง ๐ฝ โˆˆ ๐ผ ) โ†’ ( ( ๐ผ ร— { ๐ด } ) โ€˜ ๐ฝ ) = ๐ด )
20 5 7 19 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐ผ ร— { ๐ด } ) โ€˜ ๐ฝ ) = ๐ด )
21 20 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ผ ร— { ๐ด } ) โ€˜ ๐ฝ ) ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) = ( ๐ด ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) )
22 11 18 21 3eqtrd โŠข ( ๐œ‘ โ†’ ( ( ๐ด โˆ™ ๐‘‹ ) โ€˜ ๐ฝ ) = ( ๐ด ยท ( ๐‘‹ โ€˜ ๐ฝ ) ) )