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=fBaseS𝑠R|xdomR|fx0RxFin
Assertion dsmmval RVSmR=S𝑠R𝑠B

Proof

Step Hyp Ref Expression
1 dsmmval.b B=fBaseS𝑠R|xdomR|fx0RxFin
2 elex RVRV
3 oveq12 s=Sr=Rs𝑠r=S𝑠R
4 eqid s𝑠r=s𝑠r
5 vex sV
6 5 a1i s=Sr=RsV
7 vex rV
8 7 a1i s=Sr=RrV
9 eqid Bases𝑠r=Bases𝑠r
10 eqidd s=Sr=Rdomr=domr
11 4 6 8 9 10 prdsbas s=Sr=RBases𝑠r=xdomrBaserx
12 3 fveq2d s=Sr=RBases𝑠r=BaseS𝑠R
13 11 12 eqtr3d s=Sr=RxdomrBaserx=BaseS𝑠R
14 simpr s=Sr=Rr=R
15 14 dmeqd s=Sr=Rdomr=domR
16 14 fveq1d s=Sr=Rrx=Rx
17 16 fveq2d s=Sr=R0rx=0Rx
18 17 neeq2d s=Sr=Rfx0rxfx0Rx
19 15 18 rabeqbidv s=Sr=Rxdomr|fx0rx=xdomR|fx0Rx
20 19 eleq1d s=Sr=Rxdomr|fx0rxFinxdomR|fx0RxFin
21 13 20 rabeqbidv s=Sr=RfxdomrBaserx|xdomr|fx0rxFin=fBaseS𝑠R|xdomR|fx0RxFin
22 21 1 eqtr4di s=Sr=RfxdomrBaserx|xdomr|fx0rxFin=B
23 3 22 oveq12d s=Sr=Rs𝑠r𝑠fxdomrBaserx|xdomr|fx0rxFin=S𝑠R𝑠B
24 df-dsmm m=sV,rVs𝑠r𝑠fxdomrBaserx|xdomr|fx0rxFin
25 ovex S𝑠R𝑠BV
26 23 24 25 ovmpoa SVRVSmR=S𝑠R𝑠B
27 reldmdsmm Reldomm
28 27 ovprc1 ¬SVSmR=
29 ress0 𝑠B=
30 28 29 eqtr4di ¬SVSmR=𝑠B
31 reldmprds Reldom𝑠
32 31 ovprc1 ¬SVS𝑠R=
33 32 oveq1d ¬SVS𝑠R𝑠B=𝑠B
34 30 33 eqtr4d ¬SVSmR=S𝑠R𝑠B
35 34 adantr ¬SVRVSmR=S𝑠R𝑠B
36 26 35 pm2.61ian RVSmR=S𝑠R𝑠B
37 2 36 syl RVSmR=S𝑠R𝑠B