5oalem4

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	5oalem3.1	$⊢ A \in S_{ℋ}$
	5oalem3.2	$⊢ B \in S_{ℋ}$
	5oalem3.3	$⊢ C \in S_{ℋ}$
	5oalem3.4	$⊢ D \in S_{ℋ}$
	5oalem3.5	$⊢ F \in S_{ℋ}$
	5oalem3.6	$⊢ G \in S_{ℋ}$
Assertion	5oalem4	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \land (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g)) \to x -_{ℎ} z \in (((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))))$

Step	Hyp	Ref	Expression
1		5oalem3.1	$⊢ A \in S_{ℋ}$
2		5oalem3.2	$⊢ B \in S_{ℋ}$
3		5oalem3.3	$⊢ C \in S_{ℋ}$
4		5oalem3.4	$⊢ D \in S_{ℋ}$
5		5oalem3.5	$⊢ F \in S_{ℋ}$
6		5oalem3.6	$⊢ G \in S_{ℋ}$
7		eqtr3	$⊢ (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g) \to x +_{ℎ} y = z +_{ℎ} w$
8	1 2 3 4	5oalem2	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z \in ((A +_{ℋ} C) \cap (B +_{ℋ} D))$
9	7 8	sylan2	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g)) \to x -_{ℎ} z \in ((A +_{ℋ} C) \cap (B +_{ℋ} D))$
10	9	adantlr	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \land (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g)) \to x -_{ℎ} z \in ((A +_{ℋ} C) \cap (B +_{ℋ} D))$
11	1 2 3 4 5 6	5oalem3	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \land (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g)) \to x -_{ℎ} z \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
12	10 11	elind	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \land (x +_{ℎ} y = f +_{ℎ} g \land z +_{ℎ} w = f +_{ℎ} g)) \to x -_{ℎ} z \in (((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))))$

Metamath Proof Explorer