Metamath Proof Explorer


Theorem dsmmval

Description: Value of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)

Ref Expression
Hypothesis dsmmval.b
|- B = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin }
Assertion dsmmval
|- ( R e. V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )

Proof

Step Hyp Ref Expression
1 dsmmval.b
 |-  B = { f e. ( Base ` ( S Xs_ R ) ) | { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin }
2 elex
 |-  ( R e. V -> R e. _V )
3 oveq12
 |-  ( ( s = S /\ r = R ) -> ( s Xs_ r ) = ( S Xs_ R ) )
4 eqid
 |-  ( s Xs_ r ) = ( s Xs_ r )
5 vex
 |-  s e. _V
6 5 a1i
 |-  ( ( s = S /\ r = R ) -> s e. _V )
7 vex
 |-  r e. _V
8 7 a1i
 |-  ( ( s = S /\ r = R ) -> r e. _V )
9 eqid
 |-  ( Base ` ( s Xs_ r ) ) = ( Base ` ( s Xs_ r ) )
10 eqidd
 |-  ( ( s = S /\ r = R ) -> dom r = dom r )
11 4 6 8 9 10 prdsbas
 |-  ( ( s = S /\ r = R ) -> ( Base ` ( s Xs_ r ) ) = X_ x e. dom r ( Base ` ( r ` x ) ) )
12 3 fveq2d
 |-  ( ( s = S /\ r = R ) -> ( Base ` ( s Xs_ r ) ) = ( Base ` ( S Xs_ R ) ) )
13 11 12 eqtr3d
 |-  ( ( s = S /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = ( Base ` ( S Xs_ R ) ) )
14 simpr
 |-  ( ( s = S /\ r = R ) -> r = R )
15 14 dmeqd
 |-  ( ( s = S /\ r = R ) -> dom r = dom R )
16 14 fveq1d
 |-  ( ( s = S /\ r = R ) -> ( r ` x ) = ( R ` x ) )
17 16 fveq2d
 |-  ( ( s = S /\ r = R ) -> ( 0g ` ( r ` x ) ) = ( 0g ` ( R ` x ) ) )
18 17 neeq2d
 |-  ( ( s = S /\ r = R ) -> ( ( f ` x ) =/= ( 0g ` ( r ` x ) ) <-> ( f ` x ) =/= ( 0g ` ( R ` x ) ) ) )
19 15 18 rabeqbidv
 |-  ( ( s = S /\ r = R ) -> { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } = { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } )
20 19 eleq1d
 |-  ( ( s = S /\ r = R ) -> ( { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin <-> { x e. dom R | ( f ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) )
21 13 20 rabeqbidv
 |-  ( ( s = S /\ r = R ) -> { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { 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 } )
22 21 1 eqtr4di
 |-  ( ( s = S /\ r = R ) -> { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } = B )
23 3 22 oveq12d
 |-  ( ( s = S /\ r = R ) -> ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) = ( ( S Xs_ R ) |`s B ) )
24 df-dsmm
 |-  (+)m = ( s e. _V , r e. _V |-> ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )
25 ovex
 |-  ( ( S Xs_ R ) |`s B ) e. _V
26 23 24 25 ovmpoa
 |-  ( ( S e. _V /\ R e. _V ) -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )
27 reldmdsmm
 |-  Rel dom (+)m
28 27 ovprc1
 |-  ( -. S e. _V -> ( S (+)m R ) = (/) )
29 ress0
 |-  ( (/) |`s B ) = (/)
30 28 29 eqtr4di
 |-  ( -. S e. _V -> ( S (+)m R ) = ( (/) |`s B ) )
31 reldmprds
 |-  Rel dom Xs_
32 31 ovprc1
 |-  ( -. S e. _V -> ( S Xs_ R ) = (/) )
33 32 oveq1d
 |-  ( -. S e. _V -> ( ( S Xs_ R ) |`s B ) = ( (/) |`s B ) )
34 30 33 eqtr4d
 |-  ( -. S e. _V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )
35 34 adantr
 |-  ( ( -. S e. _V /\ R e. _V ) -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )
36 26 35 pm2.61ian
 |-  ( R e. _V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )
37 2 36 syl
 |-  ( R e. V -> ( S (+)m R ) = ( ( S Xs_ R ) |`s B ) )