3oalem1

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3oalem1.1	$⊢ B \in C_{ℋ}$
	3oalem1.2	$⊢ C \in C_{ℋ}$
	3oalem1.3	$⊢ R \in C_{ℋ}$
	3oalem1.4	$⊢ S \in C_{ℋ}$
Assertion	3oalem1	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ))$

Step	Hyp	Ref	Expression
1		3oalem1.1	$⊢ B \in C_{ℋ}$
2		3oalem1.2	$⊢ C \in C_{ℋ}$
3		3oalem1.3	$⊢ R \in C_{ℋ}$
4		3oalem1.4	$⊢ S \in C_{ℋ}$
5	1	cheli	$⊢ x \in B \to x \in ℋ$
6	3	cheli	$⊢ y \in R \to y \in ℋ$
7	5 6	anim12i	$⊢ (x \in B \land y \in R) \to (x \in ℋ \land y \in ℋ)$
8		hvaddcl	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y \in ℋ$
9		eleq1	$⊢ v = x +_{ℎ} y \to (v \in ℋ \leftrightarrow x +_{ℎ} y \in ℋ)$
10	8 9	syl5ibrcom	$⊢ (x \in ℋ \land y \in ℋ) \to (v = x +_{ℎ} y \to v \in ℋ)$
11	10	imdistani	$⊢ ((x \in ℋ \land y \in ℋ) \land v = x +_{ℎ} y) \to ((x \in ℋ \land y \in ℋ) \land v \in ℋ)$
12	7 11	sylan	$⊢ ((x \in B \land y \in R) \land v = x +_{ℎ} y) \to ((x \in ℋ \land y \in ℋ) \land v \in ℋ)$
13	2	cheli	$⊢ z \in C \to z \in ℋ$
14	4	cheli	$⊢ w \in S \to w \in ℋ$
15	13 14	anim12i	$⊢ (z \in C \land w \in S) \to (z \in ℋ \land w \in ℋ)$
16	15	adantr	$⊢ ((z \in C \land w \in S) \land v = z +_{ℎ} w) \to (z \in ℋ \land w \in ℋ)$
17	12 16	anim12i	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ))$

Metamath Proof Explorer