5oalem7

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000) TODO: replace uses of ee4anv with 4exdistrv as in 3oalem3 . (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	5oalem7	$⊢ ((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} S)) \subseteq 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		ee4anv	$⊢ \exists x \exists y \exists f \exists g (\exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u))) \leftrightarrow (\exists x \exists y \exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists f \exists g \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
10		exrot4	$⊢ \exists z \exists w \exists f \exists g \exists v \exists u ((((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))) \leftrightarrow \exists f \exists g \exists z \exists w \exists v \exists u ((((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)))$
11		ee4anv	$⊢ \exists z \exists w \exists v \exists u ((((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))) \leftrightarrow (\exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
12	11	2exbii	$⊢ \exists f \exists g \exists z \exists w \exists v \exists u ((((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))) \leftrightarrow \exists f \exists g (\exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
13	10 12	bitri	$⊢ \exists z \exists w \exists f \exists g \exists v \exists u ((((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))) \leftrightarrow \exists f \exists g (\exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
14	13	2exbii	$⊢ \exists x \exists y \exists z \exists w \exists f \exists g \exists v \exists u ((((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))) \leftrightarrow \exists x \exists y \exists f \exists g (\exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
15		elin	$⊢ h \in (((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} S))) \leftrightarrow (h \in ((A +_{ℋ} B) \cap (C +_{ℋ} D)) \land h \in ((F +_{ℋ} G) \cap (R +_{ℋ} S)))$
16	1 2	shseli	$⊢ h \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B h = x +_{ℎ} y$
17		r2ex	$⊢ \exists x \in A \exists y \in B h = x +_{ℎ} y \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land h = x +_{ℎ} y)$
18	16 17	bitri	$⊢ h \in (A +_{ℋ} B) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land h = x +_{ℎ} y)$
19	3 4	shseli	$⊢ h \in (C +_{ℋ} D) \leftrightarrow \exists z \in C \exists w \in D h = z +_{ℎ} w$
20		r2ex	$⊢ \exists z \in C \exists w \in D h = z +_{ℎ} w \leftrightarrow \exists z \exists w ((z \in C \land w \in D) \land h = z +_{ℎ} w)$
21	19 20	bitri	$⊢ h \in (C +_{ℋ} D) \leftrightarrow \exists z \exists w ((z \in C \land w \in D) \land h = z +_{ℎ} w)$
22	18 21	anbi12i	$⊢ (h \in (A +_{ℋ} B) \land h \in (C +_{ℋ} D)) \leftrightarrow (\exists x \exists y ((x \in A \land y \in B) \land h = x +_{ℎ} y) \land \exists z \exists w ((z \in C \land w \in D) \land h = z +_{ℎ} w))$
23		elin	$⊢ h \in ((A +_{ℋ} B) \cap (C +_{ℋ} D)) \leftrightarrow (h \in (A +_{ℋ} B) \land h \in (C +_{ℋ} D))$
24		ee4anv	$⊢ \exists x \exists y \exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \leftrightarrow (\exists x \exists y ((x \in A \land y \in B) \land h = x +_{ℎ} y) \land \exists z \exists w ((z \in C \land w \in D) \land h = z +_{ℎ} w))$
25	22 23 24	3bitr4ri	$⊢ \exists x \exists y \exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \leftrightarrow h \in ((A +_{ℋ} B) \cap (C +_{ℋ} D))$
26	5 6	shseli	$⊢ h \in (F +_{ℋ} G) \leftrightarrow \exists f \in F \exists g \in G h = f +_{ℎ} g$
27		r2ex	$⊢ \exists f \in F \exists g \in G h = f +_{ℎ} g \leftrightarrow \exists f \exists g ((f \in F \land g \in G) \land h = f +_{ℎ} g)$
28	26 27	bitri	$⊢ h \in (F +_{ℋ} G) \leftrightarrow \exists f \exists g ((f \in F \land g \in G) \land h = f +_{ℎ} g)$
29	7 8	shseli	$⊢ h \in (R +_{ℋ} S) \leftrightarrow \exists v \in R \exists u \in S h = v +_{ℎ} u$
30		r2ex	$⊢ \exists v \in R \exists u \in S h = v +_{ℎ} u \leftrightarrow \exists v \exists u ((v \in R \land u \in S) \land h = v +_{ℎ} u)$
31	29 30	bitri	$⊢ h \in (R +_{ℋ} S) \leftrightarrow \exists v \exists u ((v \in R \land u \in S) \land h = v +_{ℎ} u)$
32	28 31	anbi12i	$⊢ (h \in (F +_{ℋ} G) \land h \in (R +_{ℋ} S)) \leftrightarrow (\exists f \exists g ((f \in F \land g \in G) \land h = f +_{ℎ} g) \land \exists v \exists u ((v \in R \land u \in S) \land h = v +_{ℎ} u))$
33		elin	$⊢ h \in ((F +_{ℋ} G) \cap (R +_{ℋ} S)) \leftrightarrow (h \in (F +_{ℋ} G) \land h \in (R +_{ℋ} S))$
34		ee4anv	$⊢ \exists f \exists g \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)) \leftrightarrow (\exists f \exists g ((f \in F \land g \in G) \land h = f +_{ℎ} g) \land \exists v \exists u ((v \in R \land u \in S) \land h = v +_{ℎ} u))$
35	32 33 34	3bitr4ri	$⊢ \exists f \exists g \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)) \leftrightarrow h \in ((F +_{ℋ} G) \cap (R +_{ℋ} S))$
36	25 35	anbi12i	$⊢ (\exists x \exists y \exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists f \exists g \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u))) \leftrightarrow (h \in ((A +_{ℋ} B) \cap (C +_{ℋ} D)) \land h \in ((F +_{ℋ} G) \cap (R +_{ℋ} S)))$
37	15 36	bitr4i	$⊢ h \in (((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} S))) \leftrightarrow (\exists x \exists y \exists z \exists w (((x \in A \land y \in B) \land h = x +_{ℎ} y) \land ((z \in C \land w \in D) \land h = z +_{ℎ} w)) \land \exists f \exists g \exists v \exists u (((f \in F \land g \in G) \land h = f +_{ℎ} g) \land ((v \in R \land u \in S) \land h = v +_{ℎ} u)))$
38	9 14 37	3bitr4ri	$⊢ h \in (((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} S))) \leftrightarrow \exists x \exists y \exists z \exists w \exists f \exists g \exists v \exists u ((((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)))$
39	1 2 3 4 5 6 7 8	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)))))))))$
40	39	exlimivv	$⊢ \exists v \exists u ((((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)))))))))$
41	40	exlimivv	$⊢ \exists f \exists g \exists v \exists u ((((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)))))))))$
42	41	exlimivv	$⊢ \exists z \exists w \exists f \exists g \exists v \exists u ((((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)))))))))$
43	42	exlimivv	$⊢ \exists x \exists y \exists z \exists w \exists f \exists g \exists v \exists u ((((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)))))))))$
44	38 43	sylbi	$⊢ h \in (((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} 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)))))))))$
45	44	ssriv	$⊢ ((A +_{ℋ} B) \cap (C +_{ℋ} D)) \cap ((F +_{ℋ} G) \cap (R +_{ℋ} S)) \subseteq 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 5oalem7

Proof