5oalem3

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	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)))$

Proof

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		anandir	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \leftrightarrow (((x \in A \land y \in B) \land (f \in F \land g \in G)) \land ((z \in C \land w \in D) \land (f \in F \land g \in G)))$
8	1 2 5 6	5oalem2	$⊢ (((x \in A \land y \in B) \land (f \in F \land g \in G)) \land x +_{ℎ} y = f +_{ℎ} g) \to x -_{ℎ} f \in ((A +_{ℋ} F) \cap (B +_{ℋ} G))$
9	3 4 5 6	5oalem2	$⊢ (((z \in C \land w \in D) \land (f \in F \land g \in G)) \land z +_{ℎ} w = f +_{ℎ} g) \to z -_{ℎ} f \in ((C +_{ℋ} F) \cap (D +_{ℋ} G))$
10	8 9	anim12i	$⊢ ((((x \in A \land y \in B) \land (f \in F \land g \in G)) \land x +_{ℎ} y = f +_{ℎ} g) \land (((z \in C \land w \in D) \land (f \in F \land g \in G)) \land z +_{ℎ} w = f +_{ℎ} g)) \to (x -_{ℎ} f \in ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \land z -_{ℎ} f \in ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
11	10	an4s	$⊢ ((((x \in A \land y \in B) \land (f \in F \land g \in G)) \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 -_{ℎ} f \in ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \land z -_{ℎ} f \in ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
12	7 11	sylanb	$⊢ ((((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 -_{ℎ} f \in ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \land z -_{ℎ} f \in ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
13	1 5	shscli	$⊢ A +_{ℋ} F \in S_{ℋ}$
14	2 6	shscli	$⊢ B +_{ℋ} G \in S_{ℋ}$
15	13 14	shincli	$⊢ (A +_{ℋ} F) \cap (B +_{ℋ} G) \in S_{ℋ}$
16	3 5	shscli	$⊢ C +_{ℋ} F \in S_{ℋ}$
17	4 6	shscli	$⊢ D +_{ℋ} G \in S_{ℋ}$
18	16 17	shincli	$⊢ (C +_{ℋ} F) \cap (D +_{ℋ} G) \in S_{ℋ}$
19	15 18	shsvsi	$⊢ (x -_{ℎ} f \in ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \land z -_{ℎ} f \in ((C +_{ℋ} F) \cap (D +_{ℋ} G))) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
20	12 19	syl	$⊢ ((((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 -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G)))$
21	1	sheli	$⊢ x \in A \to x \in ℋ$
22	21	adantr	$⊢ (x \in A \land y \in B) \to x \in ℋ$
23	3	sheli	$⊢ z \in C \to z \in ℋ$
24	23	adantr	$⊢ (z \in C \land w \in D) \to z \in ℋ$
25	22 24	anim12i	$⊢ ((x \in A \land y \in B) \land (z \in C \land w \in D)) \to (x \in ℋ \land z \in ℋ)$
26	5	sheli	$⊢ f \in F \to f \in ℋ$
27	26	adantr	$⊢ (f \in F \land g \in G) \to f \in ℋ$
28		hvsubsub4	$⊢ ((x \in ℋ \land f \in ℋ) \land (z \in ℋ \land f \in ℋ)) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f)$
29	28	anandirs	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f)$
30		hvsubid	$⊢ f \in ℋ \to f -_{ℎ} f = 0_{ℎ}$
31	30	oveq2d	$⊢ f \in ℋ \to (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} 0_{ℎ}$
32		hvsubcl	$⊢ (x \in ℋ \land z \in ℋ) \to x -_{ℎ} z \in ℋ$
33		hvsub0	$⊢ x -_{ℎ} z \in ℋ \to (x -_{ℎ} z) -_{ℎ} 0_{ℎ} = x -_{ℎ} z$
34	32 33	syl	$⊢ (x \in ℋ \land z \in ℋ) \to (x -_{ℎ} z) -_{ℎ} 0_{ℎ} = x -_{ℎ} z$
35	31 34	sylan9eqr	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f) = x -_{ℎ} z$
36	29 35	eqtrd	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = x -_{ℎ} z$
37	25 27 36	syl2an	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = x -_{ℎ} z$
38	37	eleq1d	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G)) \to ((x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))) \leftrightarrow x -_{ℎ} z \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))))$
39	38	adantr	$⊢ ((((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 -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))) \leftrightarrow x -_{ℎ} z \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) +_{ℋ} ((C +_{ℋ} F) \cap (D +_{ℋ} G))))$
40	20 39	mpbid	$⊢ ((((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)))$

Metamath Proof Explorer

Theorem 5oalem3

Proof