Theorem pmodN

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

	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	pmodN	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\cap \left(Y\underset{\dot{}}{+}\left(X\cap Z\right)\right)=\left(X\cap Y\right)\underset{\dot{}}{+}\left(X\cap Z\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		incom	$$⊢X\cap \left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)=\left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)\cap X$$
5		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
6	5	adantr	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to K\in \mathrm{Lat}$$
7		simpr2	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Y\subseteq A$$
8		inss2	$$⊢X\cap Z\subseteq Z$$
9		simpr3	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Z\subseteq A$$
10	8 9	sstrid	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\cap Z\subseteq A$$
11	1 3	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge Y\subseteq A\wedge X\cap Z\subseteq A\right)\to Y\underset{\dot{}}{+}\left(X\cap Z\right)=\left(X\cap Z\right)\underset{\dot{}}{+}Y$$
12	6 7 10 11	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Y\underset{\dot{}}{+}\left(X\cap Z\right)=\left(X\cap Z\right)\underset{\dot{}}{+}Y$$
13	12	ineq2d	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\cap \left(Y\underset{\dot{}}{+}\left(X\cap Z\right)\right)=X\cap \left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)$$
14		incom	$$⊢X\cap Y=Y\cap X$$
15	14	oveq2i	$$⊢\left(X\cap Z\right)\underset{\dot{}}{+}\left(X\cap Y\right)=\left(X\cap Z\right)\underset{\dot{}}{+}\left(Y\cap X\right)$$
16		inss2	$$⊢X\cap Y\subseteq Y$$
17	16 7	sstrid	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\cap Y\subseteq A$$
18	1 3	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge X\cap Y\subseteq A\wedge X\cap Z\subseteq A\right)\to \left(X\cap Y\right)\underset{\dot{}}{+}\left(X\cap Z\right)=\left(X\cap Z\right)\underset{\dot{}}{+}\left(X\cap Y\right)$$
19	6 17 10 18	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\cap Y\right)\underset{\dot{}}{+}\left(X\cap Z\right)=\left(X\cap Z\right)\underset{\dot{}}{+}\left(X\cap Y\right)$$
20		simpr1	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\in S$$
21	10 7 20	3jca	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\cap Z\subseteq A\wedge Y\subseteq A\wedge X\in S\right)$$
22		inss1	$$⊢X\cap Z\subseteq X$$
23	1 2 3	pmod1i	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\cap Z\subseteq A\wedge Y\subseteq A\wedge X\in S\right)\right)\to \left(X\cap Z\subseteq X\to \left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)\cap X=\left(X\cap Z\right)\underset{\dot{}}{+}\left(Y\cap X\right)\right)$$
24	22 23	mpi	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\cap Z\subseteq A\wedge Y\subseteq A\wedge X\in S\right)\right)\to \left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)\cap X=\left(X\cap Z\right)\underset{\dot{}}{+}\left(Y\cap X\right)$$
25	21 24	syldan	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)\cap X=\left(X\cap Z\right)\underset{\dot{}}{+}\left(Y\cap X\right)$$
26	15 19 25	3eqtr4a	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\cap Y\right)\underset{\dot{}}{+}\left(X\cap Z\right)=\left(\left(X\cap Z\right)\underset{\dot{}}{+}Y\right)\cap X$$
27	4 13 26	3eqtr4a	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\in S\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\cap \left(Y\underset{\dot{}}{+}\left(X\cap Z\right)\right)=\left(X\cap Y\right)\underset{\dot{}}{+}\left(X\cap Z\right)$$