Metamath Proof Explorer

Theorem dsmmval2

Description: Self-referential definition of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis dsmmval2.b 
|- B = ( Base ` ( S (+)m R ) )
Assertion dsmmval2 
|- ( S (+)m R ) = ( ( S Xs_ R ) |`s B )

Proof

Step Hyp Ref Expression
1 dsmmval2.b 
 |-  B = ( Base ` ( S (+)m R ) )
2 ssrab2 
 |-  { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } C_ ( Base ` ( S Xs_ R ) )
3 eqid 
 |-  ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) = ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } )
4 eqid 
 |-  ( Base ` ( S Xs_ R ) ) = ( Base ` ( S Xs_ R ) )
5 3 4 ressbas2 
 |-  ( { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } C_ ( Base ` ( S Xs_ R ) ) -> { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = ( Base ` ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) ) )
6 2 5 ax-mp 
 |-  { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = ( Base ` ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) )
7 6 oveq2i 
 |-  ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) = ( ( S Xs_ R ) |`s ( Base ` ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) ) )
8 eqid 
 |-  { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin }
9 8 dsmmval 
 |-  ( R e. _V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) )
10 9 fveq2d 
 |-  ( R e. _V -> ( Base ` ( S (+)m R ) ) = ( Base ` ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) ) )
11 10 oveq2d 
 |-  ( R e. _V -> ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) = ( ( S Xs_ R ) |`s ( Base ` ( ( S Xs_ R ) |`s { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin } ) ) ) )
12 7 9 11 3eqtr4a 
 |-  ( R e. _V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) )
13 ress0 
 |-  ( (/) |`s ( Base ` ( S (+)m R ) ) ) = (/)
14 13 eqcomi 
 |-  (/) = ( (/) |`s ( Base ` ( S (+)m R ) ) )
15 reldmdsmm 
 |-  Rel dom (+)m
16 15 ovprc2 
 |-  ( -. R e. _V -> ( S (+)m R ) = (/) )
17 reldmprds 
 |-  Rel dom Xs_
18 17 ovprc2 
 |-  ( -. R e. _V -> ( S Xs_ R ) = (/) )
19 18 oveq1d 
 |-  ( -. R e. _V -> ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) = ( (/) |`s ( Base ` ( S (+)m R ) ) ) )
20 14 16 19 3eqtr4a 
 |-  ( -. R e. _V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) ) )
21 12 20 pm2.61i 
 |-  ( S (+)m R ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) )
22 1 oveq2i 
 |-  ( ( S Xs_ R ) |`s B ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) )
23 21 22 eqtr4i 
 |-  ( S (+)m R ) = ( ( S Xs_ R ) |`s B )