axtgeucl

Description: Euclid's Axiom. Axiom A10 of Schwabhauser p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019)

	Ref	Expression
Hypotheses	axtrkge.p	$⊢ P = {Base}_{G}$
	axtrkge.d	$⊢ \underset{˙}{-} = dist (G)$
	axtrkge.i	$⊢ I = Itv (G)$
	axtgeucl.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	axtgeucl.1	$⊢ φ \to X \in P$
	axtgeucl.2	$⊢ φ \to Y \in P$
	axtgeucl.3	$⊢ φ \to Z \in P$
	axtgeucl.4	$⊢ φ \to U \in P$
	axtgeucl.5	$⊢ φ \to V \in P$
	axtgeucl.6	$⊢ φ \to U \in (X I V)$
	axtgeucl.7	$⊢ φ \to U \in (Y I Z)$
	axtgeucl.8	$⊢ φ \to X \neq U$
Assertion	axtgeucl	$⊢ φ \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b))$

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	$⊢ P = {Base}_{G}$
2		axtrkge.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkge.i	$⊢ I = Itv (G)$
4		axtgeucl.g	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
5		axtgeucl.1	$⊢ φ \to X \in P$
6		axtgeucl.2	$⊢ φ \to Y \in P$
7		axtgeucl.3	$⊢ φ \to Z \in P$
8		axtgeucl.4	$⊢ φ \to U \in P$
9		axtgeucl.5	$⊢ φ \to V \in P$
10		axtgeucl.6	$⊢ φ \to U \in (X I V)$
11		axtgeucl.7	$⊢ φ \to U \in (Y I Z)$
12		axtgeucl.8	$⊢ φ \to X \neq U$
13	1 2 3	istrkge	$⊢ G \in 𝒢_{Tarski}^{E} \leftrightarrow (G \in V \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
14	4 13	sylib	$⊢ φ \to (G \in V \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))))$
15	14	simprd	$⊢ φ \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b)))$
16		oveq1	$⊢ x = X \to x I v = X I v$
17	16	eleq2d	$⊢ x = X \to (u \in (x I v) \leftrightarrow u \in (X I v))$
18		neeq1	$⊢ x = X \to (x \neq u \leftrightarrow X \neq u)$
19	17 18	3anbi13d	$⊢ x = X \to ((u \in (x I v) \land u \in (y I z) \land x \neq u) \leftrightarrow (u \in (X I v) \land u \in (y I z) \land X \neq u))$
20		oveq1	$⊢ x = X \to x I a = X I a$
21	20	eleq2d	$⊢ x = X \to (y \in (x I a) \leftrightarrow y \in (X I a))$
22		oveq1	$⊢ x = X \to x I b = X I b$
23	22	eleq2d	$⊢ x = X \to (z \in (x I b) \leftrightarrow z \in (X I b))$
24	21 23	3anbi12d	$⊢ x = X \to ((y \in (x I a) \land z \in (x I b) \land v \in (a I b)) \leftrightarrow (y \in (X I a) \land z \in (X I b) \land v \in (a I b)))$
25	24	2rexbidv	$⊢ x = X \to (\exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b)) \leftrightarrow \exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b)))$
26	19 25	imbi12d	$⊢ x = X \to (((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))) \leftrightarrow ((u \in (X I v) \land u \in (y I z) \land X \neq u) \to \exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b))))$
27	26	2ralbidv	$⊢ x = X \to (\forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (y I z) \land X \neq u) \to \exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b))))$
28		oveq1	$⊢ y = Y \to y I z = Y I z$
29	28	eleq2d	$⊢ y = Y \to (u \in (y I z) \leftrightarrow u \in (Y I z))$
30	29	3anbi2d	$⊢ y = Y \to ((u \in (X I v) \land u \in (y I z) \land X \neq u) \leftrightarrow (u \in (X I v) \land u \in (Y I z) \land X \neq u))$
31		eleq1	$⊢ y = Y \to (y \in (X I a) \leftrightarrow Y \in (X I a))$
32	31	3anbi1d	$⊢ y = Y \to ((y \in (X I a) \land z \in (X I b) \land v \in (a I b)) \leftrightarrow (Y \in (X I a) \land z \in (X I b) \land v \in (a I b)))$
33	32	2rexbidv	$⊢ y = Y \to (\exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b)) \leftrightarrow \exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b)))$
34	30 33	imbi12d	$⊢ y = Y \to (((u \in (X I v) \land u \in (y I z) \land X \neq u) \to \exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b))) \leftrightarrow ((u \in (X I v) \land u \in (Y I z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b))))$
35	34	2ralbidv	$⊢ y = Y \to (\forall u \in P \forall v \in P ((u \in (X I v) \land u \in (y I z) \land X \neq u) \to \exists a \in P \exists b \in P (y \in (X I a) \land z \in (X I b) \land v \in (a I b))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b))))$
36		oveq2	$⊢ z = Z \to Y I z = Y I Z$
37	36	eleq2d	$⊢ z = Z \to (u \in (Y I z) \leftrightarrow u \in (Y I Z))$
38	37	3anbi2d	$⊢ z = Z \to ((u \in (X I v) \land u \in (Y I z) \land X \neq u) \leftrightarrow (u \in (X I v) \land u \in (Y I Z) \land X \neq u))$
39		eleq1	$⊢ z = Z \to (z \in (X I b) \leftrightarrow Z \in (X I b))$
40	39	3anbi2d	$⊢ z = Z \to ((Y \in (X I a) \land z \in (X I b) \land v \in (a I b)) \leftrightarrow (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b)))$
41	40	2rexbidv	$⊢ z = Z \to (\exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b)) \leftrightarrow \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b)))$
42	38 41	imbi12d	$⊢ z = Z \to (((u \in (X I v) \land u \in (Y I z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b))) \leftrightarrow ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))))$
43	42	2ralbidv	$⊢ z = Z \to (\forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land z \in (X I b) \land v \in (a I b))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))))$
44	27 35 43	rspc3v	$⊢ (X \in P \land Y \in P \land Z \in P) \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))) \to \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))))$
45	5 6 7 44	syl3anc	$⊢ φ \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I v) \land u \in (y I z) \land x \neq u) \to \exists a \in P \exists b \in P (y \in (x I a) \land z \in (x I b) \land v \in (a I b))) \to \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))))$
46	15 45	mpd	$⊢ φ \to \forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b)))$
47		eleq1	$⊢ u = U \to (u \in (X I v) \leftrightarrow U \in (X I v))$
48		eleq1	$⊢ u = U \to (u \in (Y I Z) \leftrightarrow U \in (Y I Z))$
49		neeq2	$⊢ u = U \to (X \neq u \leftrightarrow X \neq U)$
50	47 48 49	3anbi123d	$⊢ u = U \to ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \leftrightarrow (U \in (X I v) \land U \in (Y I Z) \land X \neq U))$
51	50	imbi1d	$⊢ u = U \to (((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))) \leftrightarrow ((U \in (X I v) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))))$
52		oveq2	$⊢ v = V \to X I v = X I V$
53	52	eleq2d	$⊢ v = V \to (U \in (X I v) \leftrightarrow U \in (X I V))$
54	53	3anbi1d	$⊢ v = V \to ((U \in (X I v) \land U \in (Y I Z) \land X \neq U) \leftrightarrow (U \in (X I V) \land U \in (Y I Z) \land X \neq U))$
55		eleq1	$⊢ v = V \to (v \in (a I b) \leftrightarrow V \in (a I b))$
56	55	3anbi3d	$⊢ v = V \to ((Y \in (X I a) \land Z \in (X I b) \land v \in (a I b)) \leftrightarrow (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b)))$
57	56	2rexbidv	$⊢ v = V \to (\exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b)) \leftrightarrow \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b)))$
58	54 57	imbi12d	$⊢ v = V \to (((U \in (X I v) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))) \leftrightarrow ((U \in (X I V) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b))))$
59	51 58	rspc2v	$⊢ (U \in P \land V \in P) \to (\forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))) \to ((U \in (X I V) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b))))$
60	8 9 59	syl2anc	$⊢ φ \to (\forall u \in P \forall v \in P ((u \in (X I v) \land u \in (Y I Z) \land X \neq u) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land v \in (a I b))) \to ((U \in (X I V) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b))))$
61	46 60	mpd	$⊢ φ \to ((U \in (X I V) \land U \in (Y I Z) \land X \neq U) \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b)))$
62	10 11 12 61	mp3and	$⊢ φ \to \exists a \in P \exists b \in P (Y \in (X I a) \land Z \in (X I b) \land V \in (a I b))$

Metamath Proof Explorer

Theorem axtgeucl

Proof