Metamath Proof Explorer


Theorem shmodsi

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 AS
shmod.2 BS
shmod.3 CS
Assertion shmodsi ACA+BCA+BC

Proof

Step Hyp Ref Expression
1 shmod.1 AS
2 shmod.2 BS
3 shmod.3 CS
4 elin zA+BCzA+BzC
5 1 2 shseli zA+BxAyBz=x+y
6 3 sheli zCz
7 1 sheli xAx
8 2 sheli yBy
9 hvsubadd zxyz-x=yx+y=z
10 6 7 8 9 syl3an zCxAyBz-x=yx+y=z
11 eqcom x+y=zz=x+y
12 10 11 bitrdi zCxAyBz-x=yz=x+y
13 12 3expb zCxAyBz-x=yz=x+y
14 3 1 shsvsi zCxAz-xC+A
15 3 1 shscomi C+A=A+C
16 14 15 eleqtrdi zCxAz-xA+C
17 1 3 shlesb1i ACA+C=C
18 17 biimpi ACA+C=C
19 18 eleq2d ACz-xA+Cz-xC
20 16 19 imbitrid ACzCxAz-xC
21 eleq1 z-x=yz-xCyC
22 21 biimpd z-x=yz-xCyC
23 20 22 sylan9 ACz-x=yzCxAyC
24 23 anim2d ACz-x=yyBzCxAyByC
25 elin yBCyByC
26 24 25 syl6ibr ACz-x=yyBzCxAyBC
27 26 ex ACz-x=yyBzCxAyBC
28 27 com13 yBzCxAz-x=yACyBC
29 28 ancoms zCxAyBz-x=yACyBC
30 29 anasss zCxAyBz-x=yACyBC
31 13 30 sylbird zCxAyBz=x+yACyBC
32 31 imp zCxAyBz=x+yACyBC
33 2 3 shincli BCS
34 1 33 shsvai xAyBCx+yA+BC
35 eleq1 z=x+yzA+BCx+yA+BC
36 34 35 imbitrrid z=x+yxAyBCzA+BC
37 36 expd z=x+yxAyBCzA+BC
38 37 com12 xAz=x+yyBCzA+BC
39 38 ad2antrl zCxAyBz=x+yyBCzA+BC
40 39 imp zCxAyBz=x+yyBCzA+BC
41 32 40 syld zCxAyBz=x+yACzA+BC
42 41 exp31 zCxAyBz=x+yACzA+BC
43 42 rexlimdvv zCxAyBz=x+yACzA+BC
44 5 43 biimtrid zCzA+BACzA+BC
45 44 com13 ACzA+BzCzA+BC
46 45 impd ACzA+BzCzA+BC
47 4 46 biimtrid ACzA+BCzA+BC
48 47 ssrdv ACA+BCA+BC