Metamath Proof Explorer

Theorem ixpsnbasval

Description: The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018)

Ref Expression
Assertion ixpsnbasval 
|- ( ( R e. V /\ X e. W ) -> X_ x e. { X } ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) } )

Proof

Step Hyp Ref Expression
1 ixpsnval 
 |-  ( X e. W -> X_ x e. { X } ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) ) } )
2 1 adantl 
 |-  ( ( R e. V /\ X e. W ) -> X_ x e. { X } ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) ) } )
3 csbfv2g 
 |-  ( X e. W -> [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` [_ X / x ]_ ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) )
4 csbfv2g 
 |-  ( X e. W -> [_ X / x ]_ ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) = ( ( { X } X. { ( ringLMod ` R ) } ) ` [_ X / x ]_ x ) )
5 csbvarg 
 |-  ( X e. W -> [_ X / x ]_ x = X )
6 5 fveq2d 
 |-  ( X e. W -> ( ( { X } X. { ( ringLMod ` R ) } ) ` [_ X / x ]_ x ) = ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) )
7 4 6 eqtrd 
 |-  ( X e. W -> [_ X / x ]_ ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) = ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) )
8 7 fveq2d 
 |-  ( X e. W -> ( Base ` [_ X / x ]_ ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) ) )
9 3 8 eqtrd 
 |-  ( X e. W -> [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) ) )
10 9 adantl 
 |-  ( ( R e. V /\ X e. W ) -> [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) ) )
11 fvexd 
 |-  ( R e. V -> ( ringLMod ` R ) e. _V )
12 11 anim1ci 
 |-  ( ( R e. V /\ X e. W ) -> ( X e. W /\ ( ringLMod ` R ) e. _V ) )
13 xpsng 
 |-  ( ( X e. W /\ ( ringLMod ` R ) e. _V ) -> ( { X } X. { ( ringLMod ` R ) } ) = { <. X , ( ringLMod ` R ) >. } )
14 12 13 syl 
 |-  ( ( R e. V /\ X e. W ) -> ( { X } X. { ( ringLMod ` R ) } ) = { <. X , ( ringLMod ` R ) >. } )
15 14 fveq1d 
 |-  ( ( R e. V /\ X e. W ) -> ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) = ( { <. X , ( ringLMod ` R ) >. } ` X ) )
16 fvsng 
 |-  ( ( X e. W /\ ( ringLMod ` R ) e. _V ) -> ( { <. X , ( ringLMod ` R ) >. } ` X ) = ( ringLMod ` R ) )
17 12 16 syl 
 |-  ( ( R e. V /\ X e. W ) -> ( { <. X , ( ringLMod ` R ) >. } ` X ) = ( ringLMod ` R ) )
18 15 17 eqtrd 
 |-  ( ( R e. V /\ X e. W ) -> ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) = ( ringLMod ` R ) )
19 18 fveq2d 
 |-  ( ( R e. V /\ X e. W ) -> ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` X ) ) = ( Base ` ( ringLMod ` R ) ) )
20 10 19 eqtrd 
 |-  ( ( R e. V /\ X e. W ) -> [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` ( ringLMod ` R ) ) )
21 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
22 20 21 eqtr4di 
 |-  ( ( R e. V /\ X e. W ) -> [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = ( Base ` R ) )
23 22 eleq2d 
 |-  ( ( R e. V /\ X e. W ) -> ( ( f ` X ) e. [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) <-> ( f ` X ) e. ( Base ` R ) ) )
24 23 anbi2d 
 |-  ( ( R e. V /\ X e. W ) -> ( ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) ) <-> ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) ) )
25 24 abbidv 
 |-  ( ( R e. V /\ X e. W ) -> { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) ) } = { f | ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) } )
26 2 25 eqtrd 
 |-  ( ( R e. V /\ X e. W ) -> X_ x e. { X } ( Base ` ( ( { X } X. { ( ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) } )