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 A S
shmod.2 B S
shmod.3 C S
Assertion shmodsi A C A + B C A + B C

Proof

Step Hyp Ref Expression
1 shmod.1 A S
2 shmod.2 B S
3 shmod.3 C S
4 elin z A + B C z A + B z C
5 1 2 shseli z A + B x A y B z = x + y
6 3 sheli z C z
7 1 sheli x A x
8 2 sheli y B y
9 hvsubadd z x y z - x = y x + y = z
10 6 7 8 9 syl3an z C x A y B z - x = y x + y = z
11 eqcom x + y = z z = x + y
12 10 11 bitrdi z C x A y B z - x = y z = x + y
13 12 3expb z C x A y B z - x = y z = x + y
14 3 1 shsvsi z C x A z - x C + A
15 3 1 shscomi C + A = A + C
16 14 15 eleqtrdi z C x A z - x A + C
17 1 3 shlesb1i A C A + C = C
18 17 biimpi A C A + C = C
19 18 eleq2d A C z - x A + C z - x C
20 16 19 syl5ib A C z C x A z - x C
21 eleq1 z - x = y z - x C y C
22 21 biimpd z - x = y z - x C y C
23 20 22 sylan9 A C z - x = y z C x A y C
24 23 anim2d A C z - x = y y B z C x A y B y C
25 elin y B C y B y C
26 24 25 syl6ibr A C z - x = y y B z C x A y B C
27 26 ex A C z - x = y y B z C x A y B C
28 27 com13 y B z C x A z - x = y A C y B C
29 28 ancoms z C x A y B z - x = y A C y B C
30 29 anasss z C x A y B z - x = y A C y B C
31 13 30 sylbird z C x A y B z = x + y A C y B C
32 31 imp z C x A y B z = x + y A C y B C
33 2 3 shincli B C S
34 1 33 shsvai x A y B C x + y A + B C
35 eleq1 z = x + y z A + B C x + y A + B C
36 34 35 syl5ibr z = x + y x A y B C z A + B C
37 36 expd z = x + y x A y B C z A + B C
38 37 com12 x A z = x + y y B C z A + B C
39 38 ad2antrl z C x A y B z = x + y y B C z A + B C
40 39 imp z C x A y B z = x + y y B C z A + B C
41 32 40 syld z C x A y B z = x + y A C z A + B C
42 41 exp31 z C x A y B z = x + y A C z A + B C
43 42 rexlimdvv z C x A y B z = x + y A C z A + B C
44 5 43 syl5bi z C z A + B A C z A + B C
45 44 com13 A C z A + B z C z A + B C
46 45 impd A C z A + B z C z A + B C
47 4 46 syl5bi A C z A + B C z A + B C
48 47 ssrdv A C A + B C A + B C