axtgsegcon

Description: Axiom of segment construction, Axiom A4 of Schwabhauser p. 11. As discussed in Axiom 4 of Tarski1999 p. 178, "The intuitive content [is that] given any line segment A B , one can construct a line segment congruent to it, starting at any point Y and going in the direction of any ray containing Y . The ray is determined by the point Y and a second point X , the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point z whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	$⊢ P = {Base}_{G}$
	axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtgsegcon.1	$⊢ φ \to X \in P$
	axtgsegcon.2	$⊢ φ \to Y \in P$
	axtgsegcon.3	$⊢ φ \to A \in P$
	axtgsegcon.4	$⊢ φ \to B \in P$
Assertion	axtgsegcon	$⊢ φ \to \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtgsegcon.1	$⊢ φ \to X \in P$
6		axtgsegcon.2	$⊢ φ \to Y \in P$
7		axtgsegcon.3	$⊢ φ \to A \in P$
8		axtgsegcon.4	$⊢ φ \to B \in P$
9		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
10		inss2	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
11		inss1	$⊢ 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \subseteq 𝒢_{Tarski}^{CB}$
12	10 11	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{CB}$
13	9 12	eqsstri	$⊢ 𝒢_{Tarski} \subseteq 𝒢_{Tarski}^{CB}$
14	13 4	sselid	$⊢ φ \to G \in 𝒢_{Tarski}^{CB}$
15	1 2 3	istrkgcb	$⊢ G \in 𝒢_{Tarski}^{CB} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \land \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b)))$
16	15	simprbi	$⊢ G \in 𝒢_{Tarski}^{CB} \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \land \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b))$
17	16	simprd	$⊢ G \in 𝒢_{Tarski}^{CB} \to \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b)$
18	14 17	syl	$⊢ φ \to \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b)$
19		oveq1	$⊢ x = X \to x I z = X I z$
20	19	eleq2d	$⊢ x = X \to (y \in (x I z) \leftrightarrow y \in (X I z))$
21	20	anbi1d	$⊢ x = X \to ((y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow (y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b))$
22	21	rexbidv	$⊢ x = X \to (\exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \exists z \in P (y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b))$
23	22	2ralbidv	$⊢ x = X \to (\forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \forall a \in P \forall b \in P \exists z \in P (y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b))$
24		eleq1	$⊢ y = Y \to (y \in (X I z) \leftrightarrow Y \in (X I z))$
25		oveq1	$⊢ y = Y \to y \underset{˙}{-} z = Y \underset{˙}{-} z$
26	25	eqeq1d	$⊢ y = Y \to (y \underset{˙}{-} z = a \underset{˙}{-} b \leftrightarrow Y \underset{˙}{-} z = a \underset{˙}{-} b)$
27	24 26	anbi12d	$⊢ y = Y \to ((y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b))$
28	27	rexbidv	$⊢ y = Y \to (\exists z \in P (y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b))$
29	28	2ralbidv	$⊢ y = Y \to (\forall a \in P \forall b \in P \exists z \in P (y \in (X I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b))$
30	23 29	rspc2v	$⊢ (X \in P \land Y \in P) \to (\forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \to \forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b))$
31	5 6 30	syl2anc	$⊢ φ \to (\forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \to \forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b))$
32	18 31	mpd	$⊢ φ \to \forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b)$
33		oveq1	$⊢ a = A \to a \underset{˙}{-} b = A \underset{˙}{-} b$
34	33	eqeq2d	$⊢ a = A \to (Y \underset{˙}{-} z = a \underset{˙}{-} b \leftrightarrow Y \underset{˙}{-} z = A \underset{˙}{-} b)$
35	34	anbi2d	$⊢ a = A \to ((Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} b))$
36	35	rexbidv	$⊢ a = A \to (\exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} b))$
37		oveq2	$⊢ b = B \to A \underset{˙}{-} b = A \underset{˙}{-} B$
38	37	eqeq2d	$⊢ b = B \to (Y \underset{˙}{-} z = A \underset{˙}{-} b \leftrightarrow Y \underset{˙}{-} z = A \underset{˙}{-} B)$
39	38	anbi2d	$⊢ b = B \to ((Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} b) \leftrightarrow (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B))$
40	39	rexbidv	$⊢ b = B \to (\exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} b) \leftrightarrow \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B))$
41	36 40	rspc2v	$⊢ (A \in P \land B \in P) \to (\forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b) \to \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B))$
42	7 8 41	syl2anc	$⊢ φ \to (\forall a \in P \forall b \in P \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = a \underset{˙}{-} b) \to \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B))$
43	32 42	mpd	$⊢ φ \to \exists z \in P (Y \in (X I z) \land Y \underset{˙}{-} z = A \underset{˙}{-} B)$

Metamath Proof Explorer

Theorem axtgsegcon

Proof