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 ) )