5oalem1

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

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

Proof

Step	Hyp	Ref	Expression
1		5oalem1.1	$⊢ A \in S_{ℋ}$
2		5oalem1.2	$⊢ B \in S_{ℋ}$
3		5oalem1.3	$⊢ C \in S_{ℋ}$
4		5oalem1.4	$⊢ R \in S_{ℋ}$
5		simplll	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to x \in A$
6	1	sheli	$⊢ x \in A \to x \in ℋ$
7	6	ad2antrr	$⊢ ((x \in A \land y \in B) \land v = x +_{ℎ} y) \to x \in ℋ$
8	3	sheli	$⊢ z \in C \to z \in ℋ$
9	8	adantr	$⊢ (z \in C \land x -_{ℎ} z \in R) \to z \in ℋ$
10		hvaddsub12	$⊢ (x \in ℋ \land z \in ℋ \land z \in ℋ) \to x +_{ℎ} (z -_{ℎ} z) = z +_{ℎ} (x -_{ℎ} z)$
11	10	3anidm23	$⊢ (x \in ℋ \land z \in ℋ) \to x +_{ℎ} (z -_{ℎ} z) = z +_{ℎ} (x -_{ℎ} z)$
12		hvsubid	$⊢ z \in ℋ \to z -_{ℎ} z = 0_{ℎ}$
13	12	oveq2d	$⊢ z \in ℋ \to x +_{ℎ} (z -_{ℎ} z) = x +_{ℎ} 0_{ℎ}$
14		ax-hvaddid	$⊢ x \in ℋ \to x +_{ℎ} 0_{ℎ} = x$
15	13 14	sylan9eqr	$⊢ (x \in ℋ \land z \in ℋ) \to x +_{ℎ} (z -_{ℎ} z) = x$
16	11 15	eqtr3d	$⊢ (x \in ℋ \land z \in ℋ) \to z +_{ℎ} (x -_{ℎ} z) = x$
17	7 9 16	syl2an	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to z +_{ℎ} (x -_{ℎ} z) = x$
18	3 4	shsvai	$⊢ (z \in C \land x -_{ℎ} z \in R) \to z +_{ℎ} (x -_{ℎ} z) \in (C +_{ℋ} R)$
19	18	adantl	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to z +_{ℎ} (x -_{ℎ} z) \in (C +_{ℋ} R)$
20	17 19	eqeltrrd	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to x \in (C +_{ℋ} R)$
21	5 20	elind	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to x \in (A \cap (C +_{ℋ} R))$
22		simpllr	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to y \in B$
23	3 4	shscli	$⊢ C +_{ℋ} R \in S_{ℋ}$
24	1 23	shincli	$⊢ A \cap (C +_{ℋ} R) \in S_{ℋ}$
25	24 2	shsvai	$⊢ (x \in (A \cap (C +_{ℋ} R)) \land y \in B) \to x +_{ℎ} y \in ((A \cap (C +_{ℋ} R)) +_{ℋ} B)$
26	24 2	shscomi	$⊢ (A \cap (C +_{ℋ} R)) +_{ℋ} B = B +_{ℋ} (A \cap (C +_{ℋ} R))$
27	25 26	eleqtrdi	$⊢ (x \in (A \cap (C +_{ℋ} R)) \land y \in B) \to x +_{ℎ} y \in (B +_{ℋ} (A \cap (C +_{ℋ} R)))$
28	21 22 27	syl2anc	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to x +_{ℎ} y \in (B +_{ℋ} (A \cap (C +_{ℋ} R)))$
29		eleq1	$⊢ v = x +_{ℎ} y \to (v \in (B +_{ℋ} (A \cap (C +_{ℋ} R))) \leftrightarrow x +_{ℎ} y \in (B +_{ℋ} (A \cap (C +_{ℋ} R))))$
30	29	ad2antlr	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to (v \in (B +_{ℋ} (A \cap (C +_{ℋ} R))) \leftrightarrow x +_{ℎ} y \in (B +_{ℋ} (A \cap (C +_{ℋ} R))))$
31	28 30	mpbird	$⊢ (((x \in A \land y \in B) \land v = x +_{ℎ} y) \land (z \in C \land x -_{ℎ} z \in R)) \to v \in (B +_{ℋ} (A \cap (C +_{ℋ} R)))$

Metamath Proof Explorer

Theorem 5oalem1

Proof