Metamath Proof Explorer


Theorem shmodi

Description: The modular law is implied by the closure of subspace sum. Part of proof 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 shmodi A + B = A B 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 1 2 3 shmodsi A C A + B C A + B C
5 ineq1 A + B = A B A + B C = A B C
6 5 sseq1d A + B = A B A + B C A + B C A B C A + B C
7 4 6 syl5ib A + B = A B A C A B C A + B C
8 7 imp A + B = A B A C A B C A + B C
9 2 3 shincli B C S
10 1 9 shsleji A + B C A B C
11 8 10 sstrdi A + B = A B A C A B C A B C