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\in {\mathbf{S}}_{\mathscr{H}}$$
	shmod.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
	shmod.3	$$⊢C\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shmodi	$$⊢\left(A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\wedge A\subseteq C\right)\to \left(A{\vee }_{\mathscr{H}}B\right)\cap C\subseteq A{\vee }_{\mathscr{H}}\left(B\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		shmod.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shmod.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		shmod.3	$$⊢C\in {\mathbf{S}}_{\mathscr{H}}$$
4	1 2 3	shmodsi	$$⊢A\subseteq C\to \left(A{+}_{\mathscr{H}}B\right)\cap C\subseteq A{+}_{\mathscr{H}}\left(B\cap C\right)$$
5		ineq1	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to \left(A{+}_{\mathscr{H}}B\right)\cap C=\left(A{\vee }_{\mathscr{H}}B\right)\cap C$$
6	5	sseq1d	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to \left(\left(A{+}_{\mathscr{H}}B\right)\cap C\subseteq A{+}_{\mathscr{H}}\left(B\cap C\right)\leftrightarrow \left(A{\vee }_{\mathscr{H}}B\right)\cap C\subseteq A{+}_{\mathscr{H}}\left(B\cap C\right)\right)$$
7	4 6	imbitrid	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to \left(A\subseteq C\to \left(A{\vee }_{\mathscr{H}}B\right)\cap C\subseteq A{+}_{\mathscr{H}}\left(B\cap C\right)\right)$$
8	7	imp	$$⊢\left(A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\wedge A\subseteq C\right)\to \left(A{\vee }_{\mathscr{H}}B\right)\cap C\subseteq A{+}_{\mathscr{H}}\left(B\cap C\right)$$
9	2 3	shincli	$$⊢B\cap C\in {\mathbf{S}}_{\mathscr{H}}$$
10	1 9	shsleji	$$⊢A{+}_{\mathscr{H}}\left(B\cap C\right)\subseteq A{\vee }_{\mathscr{H}}\left(B\cap C\right)$$
11	8 10	sstrdi	$$⊢\left(A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\wedge A\subseteq C\right)\to \left(A{\vee }_{\mathscr{H}}B\right)\cap C\subseteq A{\vee }_{\mathscr{H}}\left(B\cap C\right)$$