Description: Value of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dsmmval.b | |
|
Assertion | dsmmval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dsmmval.b | |
|
2 | elex | |
|
3 | oveq12 | |
|
4 | eqid | |
|
5 | vex | |
|
6 | 5 | a1i | |
7 | vex | |
|
8 | 7 | a1i | |
9 | eqid | |
|
10 | eqidd | |
|
11 | 4 6 8 9 10 | prdsbas | |
12 | 3 | fveq2d | |
13 | 11 12 | eqtr3d | |
14 | simpr | |
|
15 | 14 | dmeqd | |
16 | 14 | fveq1d | |
17 | 16 | fveq2d | |
18 | 17 | neeq2d | |
19 | 15 18 | rabeqbidv | |
20 | 19 | eleq1d | |
21 | 13 20 | rabeqbidv | |
22 | 21 1 | eqtr4di | |
23 | 3 22 | oveq12d | |
24 | df-dsmm | |
|
25 | ovex | |
|
26 | 23 24 25 | ovmpoa | |
27 | reldmdsmm | |
|
28 | 27 | ovprc1 | |
29 | ress0 | |
|
30 | 28 29 | eqtr4di | |
31 | reldmprds | |
|
32 | 31 | ovprc1 | |
33 | 32 | oveq1d | |
34 | 30 33 | eqtr4d | |
35 | 34 | adantr | |
36 | 26 35 | pm2.61ian | |
37 | 2 36 | syl | |