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