This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrvscaval

Description: The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrvsca.s 
|- S = ( I mPwSer R )
psrvsca.n 
|- .xb = ( .s ` S )
psrvsca.k 
|- K = ( Base ` R )
psrvsca.b 
|- B = ( Base ` S )
psrvsca.m 
|- .x. = ( .r ` R )
psrvsca.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psrvsca.x 
|- ( ph -> X e. K )
psrvsca.y 
|- ( ph -> F e. B )
psrvscaval.y 
|- ( ph -> Y e. D )
Assertion psrvscaval 
|- ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 psrvsca.s 
 |-  S = ( I mPwSer R )
2 psrvsca.n 
 |-  .xb = ( .s ` S )
3 psrvsca.k 
 |-  K = ( Base ` R )
4 psrvsca.b 
 |-  B = ( Base ` S )
5 psrvsca.m 
 |-  .x. = ( .r ` R )
6 psrvsca.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 psrvsca.x 
 |-  ( ph -> X e. K )
8 psrvsca.y 
 |-  ( ph -> F e. B )
9 psrvscaval.y 
 |-  ( ph -> Y e. D )
10 1 2 3 4 5 6 7 8 psrvsca 
 |-  ( ph -> ( X .xb F ) = ( ( D X. { X } ) oF .x. F ) )
11 10 fveq1d 
 |-  ( ph -> ( ( X .xb F ) ` Y ) = ( ( ( D X. { X } ) oF .x. F ) ` Y ) )
12 ovex 
 |-  ( NN0 ^m I ) e. _V
13 6 12 rabex2 
 |-  D e. _V
14 13 a1i 
 |-  ( ph -> D e. _V )
15 1 3 6 4 8 psrelbas 
 |-  ( ph -> F : D --> K )
16 15 ffnd 
 |-  ( ph -> F Fn D )
17 eqidd 
 |-  ( ( ph /\ Y e. D ) -> ( F ` Y ) = ( F ` Y ) )
18 14 7 16 17 ofc1 
 |-  ( ( ph /\ Y e. D ) -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
19 9 18 mpdan 
 |-  ( ph -> ( ( ( D X. { X } ) oF .x. F ) ` Y ) = ( X .x. ( F ` Y ) ) )
20 11 19 eqtrd 
 |-  ( ph -> ( ( X .xb F ) ` Y ) = ( X .x. ( F ` Y ) ) )