5oalem6

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-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	5oalem6	$⊢ ((((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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		an4	$⊢ (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \leftrightarrow (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (h = x +_{ℎ} y \land h = z +_{ℎ} w))$
10		an4	$⊢ (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)) \leftrightarrow (((f \in F \land g \in G) \land (v \in R \land u \in S)) \land (h = f +_{ℎ} g \land h = v +_{ℎ} u))$
11		eqeq1	$⊢ h = x +_{ℎ} y \to (h = v +_{ℎ} u \leftrightarrow x +_{ℎ} y = v +_{ℎ} u)$
12	11	biimpcd	$⊢ h = v +_{ℎ} u \to (h = x +_{ℎ} y \to x +_{ℎ} y = v +_{ℎ} u)$
13		eqeq1	$⊢ h = z +_{ℎ} w \to (h = v +_{ℎ} u \leftrightarrow z +_{ℎ} w = v +_{ℎ} u)$
14	13	biimpcd	$⊢ h = v +_{ℎ} u \to (h = z +_{ℎ} w \to z +_{ℎ} w = v +_{ℎ} u)$
15	12 14	anim12d	$⊢ h = v +_{ℎ} u \to ((h = x +_{ℎ} y \land h = z +_{ℎ} w) \to (x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u))$
16		eqeq1	$⊢ h = f +_{ℎ} g \to (h = v +_{ℎ} u \leftrightarrow f +_{ℎ} g = v +_{ℎ} u)$
17	16	biimpcd	$⊢ h = v +_{ℎ} u \to (h = f +_{ℎ} g \to f +_{ℎ} g = v +_{ℎ} u)$
18	15 17	anim12d	$⊢ h = v +_{ℎ} u \to (((h = x +_{ℎ} y \land h = z +_{ℎ} w) \land h = f +_{ℎ} g) \to ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u))$
19	18	expdcom	$⊢ (h = x +_{ℎ} y \land h = z +_{ℎ} w) \to (h = f +_{ℎ} g \to (h = v +_{ℎ} u \to ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)))$
20	19	imp32	$⊢ ((h = x +_{ℎ} y \land h = z +_{ℎ} w) \land (h = f +_{ℎ} g \land h = v +_{ℎ} u)) \to ((x +_{ℎ} y = v +_{ℎ} u \land z +_{ℎ} w = v +_{ℎ} u) \land f +_{ℎ} g = v +_{ℎ} u)$
21	20	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))) \land ((h = x +_{ℎ} y \land h = z +_{ℎ} w) \land (h = f +_{ℎ} g \land h = v +_{ℎ} u))) \to ((((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))$
22	21	an4s	$⊢ ((((x \in A \land y \in B) \land (z \in C \land w \in D)) \land (h = x +_{ℎ} y \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land (v \in R \land u \in S)) \land (h = f +_{ℎ} g \land h = v +_{ℎ} u))) \to ((((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))$
23	9 10 22	syl2anb	$⊢ ((((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u))) \to ((((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))$
24	1 2 3 4 5 6 7 8	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))))))$
25	23 24	syl	$⊢ ((((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = 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))))))$
26	1 3	shscli	$⊢ A +_{ℋ} C \in S_{ℋ}$
27	2 4	shscli	$⊢ B +_{ℋ} D \in S_{ℋ}$
28	26 27	shincli	$⊢ (A +_{ℋ} C) \cap (B +_{ℋ} D) \in S_{ℋ}$
29	1 7	shscli	$⊢ A +_{ℋ} R \in S_{ℋ}$
30	2 8	shscli	$⊢ B +_{ℋ} S \in S_{ℋ}$
31	29 30	shincli	$⊢ (A +_{ℋ} R) \cap (B +_{ℋ} S) \in S_{ℋ}$
32	3 7	shscli	$⊢ C +_{ℋ} R \in S_{ℋ}$
33	4 8	shscli	$⊢ D +_{ℋ} S \in S_{ℋ}$
34	32 33	shincli	$⊢ (C +_{ℋ} R) \cap (D +_{ℋ} S) \in S_{ℋ}$
35	31 34	shscli	$⊢ ((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((C +_{ℋ} R) \cap (D +_{ℋ} S)) \in S_{ℋ}$
36	28 35	shincli	$⊢ ((A +_{ℋ} C) \cap (B +_{ℋ} D)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((C +_{ℋ} R) \cap (D +_{ℋ} S))) \in S_{ℋ}$
37	1 5	shscli	$⊢ A +_{ℋ} F \in S_{ℋ}$
38	2 6	shscli	$⊢ B +_{ℋ} G \in S_{ℋ}$
39	37 38	shincli	$⊢ (A +_{ℋ} F) \cap (B +_{ℋ} G) \in S_{ℋ}$
40	5 7	shscli	$⊢ F +_{ℋ} R \in S_{ℋ}$
41	6 8	shscli	$⊢ G +_{ℋ} S \in S_{ℋ}$
42	40 41	shincli	$⊢ (F +_{ℋ} R) \cap (G +_{ℋ} S) \in S_{ℋ}$
43	31 42	shscli	$⊢ ((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)) \in S_{ℋ}$
44	39 43	shincli	$⊢ ((A +_{ℋ} F) \cap (B +_{ℋ} G)) \cap (((A +_{ℋ} R) \cap (B +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))) \in S_{ℋ}$
45	3 5	shscli	$⊢ C +_{ℋ} F \in S_{ℋ}$
46	4 6	shscli	$⊢ D +_{ℋ} G \in S_{ℋ}$
47	45 46	shincli	$⊢ (C +_{ℋ} F) \cap (D +_{ℋ} G) \in S_{ℋ}$
48	34 42	shscli	$⊢ ((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S)) \in S_{ℋ}$
49	47 48	shincli	$⊢ ((C +_{ℋ} F) \cap (D +_{ℋ} G)) \cap (((C +_{ℋ} R) \cap (D +_{ℋ} S)) +_{ℋ} ((F +_{ℋ} R) \cap (G +_{ℋ} S))) \in S_{ℋ}$
50	44 49	shscli	$⊢ (((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)))) \in S_{ℋ}$
51	36 50	shincli	$⊢ (((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))))) \in S_{ℋ}$
52	1 2 3 51	5oalem1	$⊢ (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land (z \in C \land 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)))))))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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)))))))))$
53	52	expr	$⊢ (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land z \in C) \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)))))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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))))))))))$
54	53	adantrr	$⊢ (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land (z \in C \land w \in D)) \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)))))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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))))))))))$
55	54	adantrr	$⊢ (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \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)))))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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))))))))))$
56	55	adantr	$⊢ ((((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = 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)))))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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))))))))))$
57	25 56	mpd	$⊢ ((((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u))) \to h \in (B +_{ℋ} (A \cap (C +_{ℋ} ((((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 5oalem6

Proof