This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Atoms (K)$
		paddass.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	Assertion	padd12N	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = Y \underset{˙}{+} (X \underset{˙}{+} Z)$

Proof

Step	Hyp	Ref	Expression
1		paddass.a	$⊢ A = Atoms (K)$
2		paddass.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		hllat	$⊢ K \in HL \to K \in Lat$
4	3	adantr	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to K \in Lat$
5		simpr1	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \subseteq A$
6		simpr2	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to Y \subseteq A$
7	1 2	paddcom	$⊢ (K \in Lat \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
8	4 5 6 7	syl3anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
9	8	oveq1d	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = (Y \underset{˙}{+} X) \underset{˙}{+} Z$
10	1 2	paddass	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Y \underset{˙}{+} Z)$
11		simpl	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to K \in HL$
12		simpr3	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to Z \subseteq A$
13	1 2	paddass	$⊢ (K \in HL \land (Y \subseteq A \land X \subseteq A \land Z \subseteq A)) \to (Y \underset{˙}{+} X) \underset{˙}{+} Z = Y \underset{˙}{+} (X \underset{˙}{+} Z)$
14	11 6 5 12 13	syl13anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (Y \underset{˙}{+} X) \underset{˙}{+} Z = Y \underset{˙}{+} (X \underset{˙}{+} Z)$
15	9 10 14	3eqtr3d	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = Y \underset{˙}{+} (X \underset{˙}{+} Z)$