Theorem paddass

Description: Projective subspace sum is associative. Equation 16.2.1 of MaedaMaeda p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011)

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

Proof

Step	Hyp	Ref	Expression
1		paddass.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		paddass.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		simpl	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to K\in \mathrm{HL}$$
4		simpr3	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Z\subseteq A$$
5		simpr2	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Y\subseteq A$$
6		simpr1	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\subseteq A$$
7	1 2	paddasslem18	$$⊢\left(K\in \mathrm{HL}\wedge \left(Z\subseteq A\wedge Y\subseteq A\wedge X\subseteq A\right)\right)\to Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\subseteq \left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
8	3 4 5 6 7	syl13anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)\subseteq \left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
9		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
10	1 2	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
11	9 10	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
12	11	3adant3r3	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
13	12	oveq1d	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z$$
14	1 2	paddssat	$$⊢\left(K\in \mathrm{HL}\wedge Y\subseteq A\wedge X\subseteq A\right)\to Y\underset{\dot{}}{+}X\subseteq A$$
15	3 5 6 14	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Y\underset{\dot{}}{+}X\subseteq A$$
16	1 2	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge Y\underset{\dot{}}{+}X\subseteq A\wedge Z\subseteq A\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
17	9 16	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge Y\underset{\dot{}}{+}X\subseteq A\wedge Z\subseteq A\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
18	3 15 4 17	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
19	13 18	eqtrd	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}X\right)$$
20	1 2	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge Y\subseteq A\wedge Z\subseteq A\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
21	9 20	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge Y\subseteq A\wedge Z\subseteq A\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
22	21	3adant3r1	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
23	22	oveq2d	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
24	1 2	paddssat	$$⊢\left(K\in \mathrm{HL}\wedge Z\subseteq A\wedge Y\subseteq A\right)\to Z\underset{\dot{}}{+}Y\subseteq A$$
25	3 4 5 24	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to Z\underset{\dot{}}{+}Y\subseteq A$$
26	1 2	paddcom	$$⊢\left(K\in \mathrm{Lat}\wedge X\subseteq A\wedge Z\underset{\dot{}}{+}Y\subseteq A\right)\to X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)=\left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
27	9 26	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Z\underset{\dot{}}{+}Y\subseteq A\right)\to X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)=\left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
28	3 6 25 27	syl3anc	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)=\left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
29	23 28	eqtrd	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=\left(Z\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}X$$
30	8 19 29	3sstr4d	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z\subseteq X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
31	1 2	paddasslem18	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)\subseteq \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z$$
32	30 31	eqssd	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$