istrkgc

Description: Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	$⊢ P = {Base}_{G}$
	istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg.i	$⊢ I = Itv (G)$
Assertion	istrkgc	$⊢ G \in 𝒢_{Tarski}^{C} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \land \forall x \in P \forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y)))$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$⊢ P = {Base}_{G}$
2		istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg.i	$⊢ I = Itv (G)$
4		simpl	$⊢ (p = P \land d = \underset{˙}{-}) \to p = P$
5	4	eqcomd	$⊢ (p = P \land d = \underset{˙}{-}) \to P = p$
6	5	adantr	$⊢ ((p = P \land d = \underset{˙}{-}) \land x \in P) \to P = p$
7		simpllr	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to d = \underset{˙}{-}$
8	7	eqcomd	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to \underset{˙}{-} = d$
9	8	oveqd	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to x \underset{˙}{-} y = x d y$
10	8	oveqd	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to y \underset{˙}{-} x = y d x$
11	9 10	eqeq12d	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to (x \underset{˙}{-} y = y \underset{˙}{-} x \leftrightarrow x d y = y d x)$
12	6 11	raleqbidva	$⊢ ((p = P \land d = \underset{˙}{-}) \land x \in P) \to (\forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \leftrightarrow \forall y \in p x d y = y d x)$
13	5 12	raleqbidva	$⊢ (p = P \land d = \underset{˙}{-}) \to (\forall x \in P \forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \leftrightarrow \forall x \in p \forall y \in p x d y = y d x)$
14	6	adantr	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to P = p$
15	8	oveqdr	$⊢ ((((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \land z \in P) \to x \underset{˙}{-} y = x d y$
16	8	oveqdr	$⊢ ((((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \land z \in P) \to z \underset{˙}{-} z = z d z$
17	15 16	eqeq12d	$⊢ ((((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \land z \in P) \to (x \underset{˙}{-} y = z \underset{˙}{-} z \leftrightarrow x d y = z d z)$
18	17	imbi1d	$⊢ ((((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \land z \in P) \to ((x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y) \leftrightarrow (x d y = z d z \to x = y))$
19	14 18	raleqbidva	$⊢ (((p = P \land d = \underset{˙}{-}) \land x \in P) \land y \in P) \to (\forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y) \leftrightarrow \forall z \in p (x d y = z d z \to x = y))$
20	6 19	raleqbidva	$⊢ ((p = P \land d = \underset{˙}{-}) \land x \in P) \to (\forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y) \leftrightarrow \forall y \in p \forall z \in p (x d y = z d z \to x = y))$
21	5 20	raleqbidva	$⊢ (p = P \land d = \underset{˙}{-}) \to (\forall x \in P \forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y) \leftrightarrow \forall x \in p \forall y \in p \forall z \in p (x d y = z d z \to x = y))$
22	13 21	anbi12d	$⊢ (p = P \land d = \underset{˙}{-}) \to ((\forall x \in P \forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \land \forall x \in P \forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y)) \leftrightarrow (\forall x \in p \forall y \in p x d y = y d x \land \forall x \in p \forall y \in p \forall z \in p (x d y = z d z \to x = y)))$
23	1 2 22	sbcie2s	$⊢ f = G \to (\underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} (\forall x \in p \forall y \in p x d y = y d x \land \forall x \in p \forall y \in p \forall z \in p (x d y = z d z \to x = y)) \leftrightarrow (\forall x \in P \forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \land \forall x \in P \forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y)))$
24		df-trkgc	$⊢ 𝒢_{Tarski}^{C} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} (\forall x \in p \forall y \in p x d y = y d x \land \forall x \in p \forall y \in p \forall z \in p (x d y = z d z \to x = y))\}$
25	23 24	elab4g	$⊢ G \in 𝒢_{Tarski}^{C} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P x \underset{˙}{-} y = y \underset{˙}{-} x \land \forall x \in P \forall y \in P \forall z \in P (x \underset{˙}{-} y = z \underset{˙}{-} z \to x = y)))$

Metamath Proof Explorer

Theorem istrkgc

Proof