pmod1i

Description: The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012)

	Ref	Expression
Hypotheses	pmod.a	$⊢ A = Atoms (K)$
	pmod.s	$⊢ S = PSubSp (K)$
	pmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmod1i	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to (X \subseteq Z \to (X \underset{˙}{+} Y) \cap Z = X \underset{˙}{+} (Y \cap Z))$

Proof

Step	Hyp	Ref	Expression
1		pmod.a	$⊢ A = Atoms (K)$
2		pmod.s	$⊢ S = PSubSp (K)$
3		pmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ join (K) = join (K)$
6	4 5 1 2 3	pmodlem2	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
7	6	3expa	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
8		inss1	$⊢ Y \cap Z \subseteq Y$
9		simpll	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to K \in HL$
10		simplr2	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Y \subseteq A$
11		simplr1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to X \subseteq A$
12	1 3	paddss2	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq A) \to (Y \cap Z \subseteq Y \to X \underset{˙}{+} (Y \cap Z) \subseteq X \underset{˙}{+} Y)$
13	9 10 11 12	syl3anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to (Y \cap Z \subseteq Y \to X \underset{˙}{+} (Y \cap Z) \subseteq X \underset{˙}{+} Y)$
14	8 13	mpi	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to X \underset{˙}{+} (Y \cap Z) \subseteq X \underset{˙}{+} Y$
15		simpl	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to K \in HL$
16	1 2	psubssat	$⊢ (K \in HL \land Z \in S) \to Z \subseteq A$
17	16	3ad2antr3	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Z \subseteq A$
18		simpr2	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Y \subseteq A$
19		ssinss1	$⊢ Y \subseteq A \to Y \cap Z \subseteq A$
20	18 19	syl	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Y \cap Z \subseteq A$
21	1 3	paddss1	$⊢ (K \in HL \land Z \subseteq A \land Y \cap Z \subseteq A) \to (X \subseteq Z \to X \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} (Y \cap Z))$
22	15 17 20 21	syl3anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to (X \subseteq Z \to X \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} (Y \cap Z))$
23	22	imp	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to X \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} (Y \cap Z)$
24		simplr3	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Z \in S$
25	9 24 16	syl2anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Z \subseteq A$
26		inss2	$⊢ Y \cap Z \subseteq Z$
27	1 3	paddss2	$⊢ (K \in HL \land Z \subseteq A \land Z \subseteq A) \to (Y \cap Z \subseteq Z \to Z \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} Z)$
28	26 27	mpi	$⊢ (K \in HL \land Z \subseteq A \land Z \subseteq A) \to Z \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} Z$
29	9 25 25 28	syl3anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Z \underset{˙}{+} (Y \cap Z) \subseteq Z \underset{˙}{+} Z$
30	2 3	paddidm	$⊢ (K \in HL \land Z \in S) \to Z \underset{˙}{+} Z = Z$
31	9 24 30	syl2anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Z \underset{˙}{+} Z = Z$
32	29 31	sseqtrd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to Z \underset{˙}{+} (Y \cap Z) \subseteq Z$
33	23 32	sstrd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to X \underset{˙}{+} (Y \cap Z) \subseteq Z$
34	14 33	ssind	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to X \underset{˙}{+} (Y \cap Z) \subseteq (X \underset{˙}{+} Y) \cap Z$
35	7 34	eqssd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \land X \subseteq Z) \to (X \underset{˙}{+} Y) \cap Z = X \underset{˙}{+} (Y \cap Z)$
36	35	ex	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to (X \subseteq Z \to (X \underset{˙}{+} Y) \cap Z = X \underset{˙}{+} (Y \cap Z))$

Metamath Proof Explorer

Theorem pmod1i

Proof