Theorem padd12N

Description: Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddass.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	paddass.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
Assertion	padd12N	$$⊢\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)=Y\underset{\dot{}}{+}\left(X\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		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
4	3	adantr	$$⊢\left(K\in \mathrm{HL}\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge Z\subseteq A\right)\right)\to K\in \mathrm{Lat}$$
5		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$$
6		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$$
7	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$$
8	4 5 6 7	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{}}{+}Y=Y\underset{\dot{}}{+}X$$
9	8	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$$
10	1 2	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)$$
11		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}$$
12		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$$
13	1 2	paddass	$$⊢\left(K\in \mathrm{HL}\wedge \left(Y\subseteq A\wedge X\subseteq A\wedge Z\subseteq A\right)\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$
14	11 6 5 12 13	syl13anc	$$⊢\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=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$
15	9 10 14	3eqtr3d	$$⊢\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)=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$