pmodN

Description: The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmod.a	$⊢ A = Atoms (K)$
	pmod.s	$⊢ S = PSubSp (K)$
	pmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmodN	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \cap (Y \underset{˙}{+} (X \cap Z)) = (X \cap Y) \underset{˙}{+} (X \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		incom	$⊢ X \cap ((X \cap Z) \underset{˙}{+} Y) = ((X \cap Z) \underset{˙}{+} Y) \cap X$
5		hllat	$⊢ K \in HL \to K \in Lat$
6	5	adantr	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to K \in Lat$
7		simpr2	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to Y \subseteq A$
8		inss2	$⊢ X \cap Z \subseteq Z$
9		simpr3	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to Z \subseteq A$
10	8 9	sstrid	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \cap Z \subseteq A$
11	1 3	paddcom	$⊢ (K \in Lat \land Y \subseteq A \land X \cap Z \subseteq A) \to Y \underset{˙}{+} (X \cap Z) = (X \cap Z) \underset{˙}{+} Y$
12	6 7 10 11	syl3anc	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to Y \underset{˙}{+} (X \cap Z) = (X \cap Z) \underset{˙}{+} Y$
13	12	ineq2d	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \cap (Y \underset{˙}{+} (X \cap Z)) = X \cap ((X \cap Z) \underset{˙}{+} Y)$
14		incom	$⊢ X \cap Y = Y \cap X$
15	14	oveq2i	$⊢ (X \cap Z) \underset{˙}{+} (X \cap Y) = (X \cap Z) \underset{˙}{+} (Y \cap X)$
16		inss2	$⊢ X \cap Y \subseteq Y$
17	16 7	sstrid	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \cap Y \subseteq A$
18	1 3	paddcom	$⊢ (K \in Lat \land X \cap Y \subseteq A \land X \cap Z \subseteq A) \to (X \cap Y) \underset{˙}{+} (X \cap Z) = (X \cap Z) \underset{˙}{+} (X \cap Y)$
19	6 17 10 18	syl3anc	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to (X \cap Y) \underset{˙}{+} (X \cap Z) = (X \cap Z) \underset{˙}{+} (X \cap Y)$
20		simpr1	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \in S$
21	10 7 20	3jca	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to (X \cap Z \subseteq A \land Y \subseteq A \land X \in S)$
22		inss1	$⊢ X \cap Z \subseteq X$
23	1 2 3	pmod1i	$⊢ (K \in HL \land (X \cap Z \subseteq A \land Y \subseteq A \land X \in S)) \to (X \cap Z \subseteq X \to ((X \cap Z) \underset{˙}{+} Y) \cap X = (X \cap Z) \underset{˙}{+} (Y \cap X))$
24	22 23	mpi	$⊢ (K \in HL \land (X \cap Z \subseteq A \land Y \subseteq A \land X \in S)) \to ((X \cap Z) \underset{˙}{+} Y) \cap X = (X \cap Z) \underset{˙}{+} (Y \cap X)$
25	21 24	syldan	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to ((X \cap Z) \underset{˙}{+} Y) \cap X = (X \cap Z) \underset{˙}{+} (Y \cap X)$
26	15 19 25	3eqtr4a	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to (X \cap Y) \underset{˙}{+} (X \cap Z) = ((X \cap Z) \underset{˙}{+} Y) \cap X$
27	4 13 26	3eqtr4a	$⊢ (K \in HL \land (X \in S \land Y \subseteq A \land Z \subseteq A)) \to X \cap (Y \underset{˙}{+} (X \cap Z)) = (X \cap Y) \underset{˙}{+} (X \cap Z)$

Metamath Proof Explorer

Theorem pmodN

Proof