5oalem5

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

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

Proof

Step	Hyp	Ref	Expression
1		5oalem5.1	$⊢ A \in S_{ℋ}$
2		5oalem5.2	$⊢ B \in S_{ℋ}$
3		5oalem5.3	$⊢ C \in S_{ℋ}$
4		5oalem5.4	$⊢ D \in S_{ℋ}$
5		5oalem5.5	$⊢ F \in S_{ℋ}$
6		5oalem5.6	$⊢ G \in S_{ℋ}$
7		5oalem5.7	$⊢ R \in S_{ℋ}$
8		5oalem5.8	$⊢ S \in S_{ℋ}$
9		simpr	$⊢ ((f \in F \land g \in G) \land (v \in R \land u \in S)) \to (v \in R \land u \in S)$
10	9	anim2i	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (v \in R \land u \in S))$
11		simpl	$⊢ ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u) \to (x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u)$
12	1 2 3 4 7 8	5oalem4	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (v \in R \land u \in S)) \land (x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u)) \to x -_{ℎ} z \in (((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((C +_{ℋ} R) \cap (D +_{ℋ} S))))$
13	10 11 12	syl2an	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to x -_{ℎ} z \in (((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((C +_{ℋ} R) \cap (D +_{ℋ} S))))$
14	1	sheli	$⊢ x \in A \to x \in ℋ$
15	14	adantr	$⊢ (x \in A \land y \in B) \to x \in ℋ$
16	3	sheli	$⊢ z \in C \to z \in ℋ$
17	16	adantr	$⊢ (z \in C \land w \in D) \to z \in ℋ$
18	15 17	anim12i	$⊢ ((x \in A \land y \in B) \land (z \in C \land w \in D)) \to (x \in ℋ \land z \in ℋ)$
19	5	sheli	$⊢ f \in F \to f \in ℋ$
20	19	adantr	$⊢ (f \in F \land g \in G) \to f \in ℋ$
21		hvsubsub4	$⊢ ((x \in ℋ \land f \in ℋ) \land (z \in ℋ \land f \in ℋ)) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f)$
22	21	anandirs	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f)$
23		hvsubid	$⊢ f \in ℋ \to f -_{ℎ} f = 0_{ℎ}$
24	23	oveq2d	$⊢ f \in ℋ \to (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f) = (x -_{ℎ} z) -_{ℎ} 0_{ℎ}$
25		hvsubcl	$⊢ (x \in ℋ \land z \in ℋ) \to x -_{ℎ} z \in ℋ$
26		hvsub0	$⊢ x -_{ℎ} z \in ℋ \to (x -_{ℎ} z) -_{ℎ} 0_{ℎ} = x -_{ℎ} z$
27	25 26	syl	$⊢ (x \in ℋ \land z \in ℋ) \to (x -_{ℎ} z) -_{ℎ} 0_{ℎ} = x -_{ℎ} z$
28	24 27	sylan9eqr	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} z) -_{ℎ} (f -_{ℎ} f) = x -_{ℎ} z$
29	22 28	eqtrd	$⊢ ((x \in ℋ \land z \in ℋ) \land f \in ℋ) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = x -_{ℎ} z$
30	18 20 29	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$
31	30	adantrr	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = x -_{ℎ} z$
32	31	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 (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) = x -_{ℎ} z$
33		simpl	$⊢ ((f \in F \land g \in G) \land (v \in R \land u \in S)) \to (f \in F \land g \in G)$
34	33	anim2i	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (f \in F \land g \in G))$
35		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)))$
36	34 35	sylib	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to (((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)))$
37		simprr	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to (v \in R \land u \in S)$
38	36 37	jca	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \to ((((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 (v \in R \land u \in S))$
39		simpl	$⊢ (x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \to x +_{ℎ} y = v +_{ℎ} u$
40	39	anim1i	$⊢ ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u) \to (x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u)$
41		simpr	$⊢ (x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \to z +_{ℎ} w = v +_{ℎ} u$
42	41	anim1i	$⊢ ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u) \to (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u)$
43	40 42	jca	$⊢ ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u) \to ((x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u) \land (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u))$
44		anandir	$⊢ ((((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 (v \in R \land u \in S)) \leftrightarrow ((((x \in A \land y \in B) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (((z \in C \land w \in D) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)))$
45	1 2 5 6 7 8	5oalem4	$⊢ ((((x \in A \land y \in B) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u)) \to x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))))$
46	3 4 5 6 7 8	5oalem4	$⊢ ((((z \in C \land w \in D) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u)) \to z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))))$
47	45 46	anim12i	$⊢ (((((x \in A \land y \in B) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u)) \land ((((z \in C \land w \in D) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u))) \to (x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) \land z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
48	47	an4s	$⊢ (((((x \in A \land y \in B) \land (f \in F \land g \in G)) \land (v \in R \land u \in S)) \land (((z \in C \land w \in D) \land (f \in F \land g \in G)) \land (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u) \land (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u))) \to (x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) \land z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
49	44 48	sylanb	$⊢ (((((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 (v \in R \land u \in S)) \land ((x +_{ℎ} y = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u) \land (z +_{ℎ} w = v +_{ℎ} u \land f +_{ℎ} g = v +_{ℎ} u))) \to (x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) \land z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
50	38 43 49	syl2an	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to (x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) \land z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
51	1 5	shscli	$⊢ A +_{ℋ} F \in S_{ℋ}$
52	2 6	shscli	$⊢ B +_{ℋ} G \in S_{ℋ}$
53	51 52	shincli	$⊢ (A +_{ℋ} F) \cap (B +_{ℋ} G) \in S_{ℋ}$
54	1 7	shscli	$⊢ A +_{ℋ} R \in S_{ℋ}$
55	2 8	shscli	$⊢ B +_{ℋ} S \in S_{ℋ}$
56	54 55	shincli	$⊢ (A +_{ℋ} R) \cap (B +_{ℋ} S) \in S_{ℋ}$
57	5 7	shscli	$⊢ F +_{ℋ} R \in S_{ℋ}$
58	6 8	shscli	$⊢ G +_{ℋ} S \in S_{ℋ}$
59	57 58	shincli	$⊢ (F +_{ℋ} R) \cap (G +_{ℋ} S) \in S_{ℋ}$
60	56 59	shscli	$⊢ ((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)) \in S_{ℋ}$
61	53 60	shincli	$⊢ ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))) \in S_{ℋ}$
62	3 5	shscli	$⊢ C +_{ℋ} F \in S_{ℋ}$
63	4 6	shscli	$⊢ D +_{ℋ} G \in S_{ℋ}$
64	62 63	shincli	$⊢ (C +_{ℋ} F) \cap (D +_{ℋ} G) \in S_{ℋ}$
65	3 7	shscli	$⊢ C +_{ℋ} R \in S_{ℋ}$
66	4 8	shscli	$⊢ D +_{ℋ} S \in S_{ℋ}$
67	65 66	shincli	$⊢ (C +_{ℋ} R) \cap (D +_{ℋ} S) \in S_{ℋ}$
68	67 59	shscli	$⊢ ((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)) \in S_{ℋ}$
69	64 68	shincli	$⊢ ((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))) \in S_{ℋ}$
70	61 69	shsvsi	$⊢ (x -_{ℎ} f \in (((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) \land z -_{ℎ} f \in (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))))) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in ((((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) +_{ℋ} (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
71	50 70	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 (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to (x -_{ℎ} f) -_{ℎ} (z -_{ℎ} f) \in ((((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) +_{ℋ} (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
72	32 71	eqeltrrd	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land ((f \in F \land g \in G) \land (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to x -_{ℎ} z \in ((((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) +_{ℋ} (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))))$
73	13 72	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 (v \in R \land u \in S))) \land ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)) \to x -_{ℎ} z \in ((((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((C +_{ℋ} R) \cap (D +_{ℋ} S)))) \cap ((((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)))) +_{ℋ} (((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))))))$

Metamath Proof Explorer

Theorem 5oalem5

Proof