Metamath Proof Explorer

Theorem dsmmfi

Description: For finite products, the direct sum is just the module product. See also the observation in Lang p. 129. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion dsmmfi 
|- ( ( R Fn I /\ I e. Fin ) -> ( S (+)m R ) = ( S Xs_ R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` ( S (+)m R ) ) = ( Base ` ( S (+)m R ) )
2 1 dsmmval2 
 |-  ( S (+)m R ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) )
3 eqid 
 |-  ( S Xs_ R ) = ( S Xs_ R )
4 eqid 
 |-  ( Base ` ( S Xs_ R ) ) = ( Base ` ( S Xs_ R ) )
5 noel 
 |-  -. f e. (/)
6 reldmprds 
 |-  Rel dom Xs_
7 6 ovprc1 
 |-  ( -. S e. _V -> ( S Xs_ R ) = (/) )
8 7 fveq2d 
 |-  ( -. S e. _V -> ( Base ` ( S Xs_ R ) ) = ( Base ` (/) ) )
9 base0 
 |-  (/) = ( Base ` (/) )
10 8 9 eqtr4di 
 |-  ( -. S e. _V -> ( Base ` ( S Xs_ R ) ) = (/) )
11 10 eleq2d 
 |-  ( -. S e. _V -> ( f e. ( Base ` ( S Xs_ R ) ) <-> f e. (/) ) )
12 5 11 mtbiri 
 |-  ( -. S e. _V -> -. f e. ( Base ` ( S Xs_ R ) ) )
13 12 con4i 
 |-  ( f e. ( Base ` ( S Xs_ R ) ) -> S e. _V )
14 13 adantl 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> S e. _V )
15 simplr 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> I e. Fin )
16 simpll 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> R Fn I )
17 simpr 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> f e. ( Base ` ( S Xs_ R ) ) )
18 3 4 14 15 16 17 prdsbasfn 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> f Fn I )
19 18 fndmd 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> dom f = I )
20 19 15 eqeltrd 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> dom f e. Fin )
21 difss 
 |-  ( f \ ( 0g o. R ) ) C_ f
22 dmss 
 |-  ( ( f \ ( 0g o. R ) ) C_ f -> dom ( f \ ( 0g o. R ) ) C_ dom f )
23 21 22 ax-mp 
 |-  dom ( f \ ( 0g o. R ) ) C_ dom f
24 ssfi 
 |-  ( ( dom f e. Fin /\ dom ( f \ ( 0g o. R ) ) C_ dom f ) -> dom ( f \ ( 0g o. R ) ) e. Fin )
25 20 23 24 sylancl 
 |-  ( ( ( R Fn I /\ I e. Fin ) /\ f e. ( Base ` ( S Xs_ R ) ) ) -> dom ( f \ ( 0g o. R ) ) e. Fin )
26 25 ralrimiva 
 |-  ( ( R Fn I /\ I e. Fin ) -> A. f e. ( Base ` ( S Xs_ R ) ) dom ( f \ ( 0g o. R ) ) e. Fin )
27 rabid2 
 |-  ( ( Base ` ( S Xs_ R ) ) = { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin } <-> A. f e. ( Base ` ( S Xs_ R ) ) dom ( f \ ( 0g o. R ) ) e. Fin )
28 26 27 sylibr 
 |-  ( ( R Fn I /\ I e. Fin ) -> ( Base ` ( S Xs_ R ) ) = { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin } )
29 eqid 
 |-  { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin }
30 3 29 dsmmbas2 
 |-  ( ( R Fn I /\ I e. Fin ) -> { f e. ( Base ` ( S Xs_ R ) ) | dom ( f \ ( 0g o. R ) ) e. Fin } = ( Base ` ( S (+)m R ) ) )
31 28 30 eqtr2d 
 |-  ( ( R Fn I /\ I e. Fin ) -> ( Base ` ( S (+)m R ) ) = ( Base ` ( S Xs_ R ) ) )
32 31 oveq2d 
 |-  ( ( R Fn I /\ I e. Fin ) -> ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) = ( ( S Xs_ R ) |`s ( Base ` ( S Xs_ R ) ) ) )
33 ovex 
 |-  ( S Xs_ R ) e. _V
34 4 ressid 
 |-  ( ( S Xs_ R ) e. _V -> ( ( S Xs_ R ) |`s ( Base ` ( S Xs_ R ) ) ) = ( S Xs_ R ) )
35 33 34 ax-mp 
 |-  ( ( S Xs_ R ) |`s ( Base ` ( S Xs_ R ) ) ) = ( S Xs_ R )
36 32 35 eqtrdi 
 |-  ( ( R Fn I /\ I e. Fin ) -> ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) = ( S Xs_ R ) )
37 2 36 eqtrid 
 |-  ( ( R Fn I /\ I e. Fin ) -> ( S (+)m R ) = ( S Xs_ R ) )