Metamath Proof Explorer

Theorem padd4N

Description: Rearrangement of 4 terms in a 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	padd4N	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$

Proof

Step	Hyp	Ref	Expression
1		paddass.a	$⊢ A = Atoms (K)$
2		paddass.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		simp1	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to K \in HL$
4		simp2r	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to Y \subseteq A$
5		simp3l	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to Z \subseteq A$
6		simp3r	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to W \subseteq A$
7	1 2	padd12N	$⊢ (K \in HL \land (Y \subseteq A \land Z \subseteq A \land W \subseteq A)) \to Y \underset{˙}{+} (Z \underset{˙}{+} W) = Z \underset{˙}{+} (Y \underset{˙}{+} W)$
8	3 4 5 6 7	syl13anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to Y \underset{˙}{+} (Z \underset{˙}{+} W) = Z \underset{˙}{+} (Y \underset{˙}{+} W)$
9	8	oveq2d	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W)) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
10		simp2l	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to X \subseteq A$
11	1 2	paddssat	$⊢ (K \in HL \land Z \subseteq A \land W \subseteq A) \to Z \underset{˙}{+} W \subseteq A$
12	3 5 6 11	syl3anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to Z \underset{˙}{+} W \subseteq A$
13	1 2	paddass	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \underset{˙}{+} W \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$
14	3 10 4 12 13	syl13anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$
15	1 2	paddssat	$⊢ (K \in HL \land Y \subseteq A \land W \subseteq A) \to Y \underset{˙}{+} W \subseteq A$
16	3 4 6 15	syl3anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to Y \underset{˙}{+} W \subseteq A$
17	1 2	paddass	$⊢ (K \in HL \land (X \subseteq A \land Z \subseteq A \land Y \underset{˙}{+} W \subseteq A)) \to (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
18	3 10 5 16 17	syl13anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
19	9 14 18	3eqtr4d	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A) \land (Z \subseteq A \land W \subseteq A)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$