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 \in S_{ℋ}$
	shmod.2	$⊢ B \in S_{ℋ}$
	shmod.3	$⊢ C \in S_{ℋ}$
Assertion	shmodsi	$⊢ A \subseteq C \to (A +_{ℋ} B) \cap C \subseteq A +_{ℋ} (B \cap C)$

Proof

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

Metamath Proof Explorer

Theorem shmodsi

Proof