Theorem pmod1i

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

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

Proof

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