Description: The modular law holds for subspace sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | shmod.1 | |
|
shmod.2 | |
||
shmod.3 | |
||
Assertion | shmodsi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shmod.1 | |
|
2 | shmod.2 | |
|
3 | shmod.3 | |
|
4 | elin | |
|
5 | 1 2 | shseli | |
6 | 3 | sheli | |
7 | 1 | sheli | |
8 | 2 | sheli | |
9 | hvsubadd | |
|
10 | 6 7 8 9 | syl3an | |
11 | eqcom | |
|
12 | 10 11 | bitrdi | |
13 | 12 | 3expb | |
14 | 3 1 | shsvsi | |
15 | 3 1 | shscomi | |
16 | 14 15 | eleqtrdi | |
17 | 1 3 | shlesb1i | |
18 | 17 | biimpi | |
19 | 18 | eleq2d | |
20 | 16 19 | imbitrid | |
21 | eleq1 | |
|
22 | 21 | biimpd | |
23 | 20 22 | sylan9 | |
24 | 23 | anim2d | |
25 | elin | |
|
26 | 24 25 | syl6ibr | |
27 | 26 | ex | |
28 | 27 | com13 | |
29 | 28 | ancoms | |
30 | 29 | anasss | |
31 | 13 30 | sylbird | |
32 | 31 | imp | |
33 | 2 3 | shincli | |
34 | 1 33 | shsvai | |
35 | eleq1 | |
|
36 | 34 35 | imbitrrid | |
37 | 36 | expd | |
38 | 37 | com12 | |
39 | 38 | ad2antrl | |
40 | 39 | imp | |
41 | 32 40 | syld | |
42 | 41 | exp31 | |
43 | 42 | rexlimdvv | |
44 | 5 43 | biimtrid | |
45 | 44 | com13 | |
46 | 45 | impd | |
47 | 4 46 | biimtrid | |
48 | 47 | ssrdv | |