istrkgcb

Description: Property of being a Tarski geometry - congruence and betweenness 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	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)))$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$⊢ P = {Base}_{G}$
2		istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg.i	$⊢ I = Itv (G)$
4		simp1	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to p = P$
5	4	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to P = p$
6	5	adantr	$⊢ ((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \to P = p$
7	6	adantr	$⊢ (((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \to P = p$
8	7	adantr	$⊢ ((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \to P = p$
9	8	adantr	$⊢ (((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \to P = p$
10	9	adantr	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \to P = p$
11	5	ad6antr	$⊢ (((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \to P = p$
12	6	ad6antr	$⊢ ((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \to P = p$
13		simpll3	$⊢ (((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \to i = I$
14	13	ad6antr	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to i = I$
15	14	eqcomd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to I = i$
16	15	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to x I z = x i z$
17	16	eleq2d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (y \in (x I z) \leftrightarrow y \in (x i z))$
18	15	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to a I c = a i c$
19	18	eleq2d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (b \in (a I c) \leftrightarrow b \in (a i c))$
20	17 19	3anbi23d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to ((x \neq y \land y \in (x I z) \land b \in (a I c)) \leftrightarrow (x \neq y \land y \in (x i z) \land b \in (a i c)))$
21		simpll2	$⊢ (((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \to d = \underset{˙}{-}$
22	21	ad6antr	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to d = \underset{˙}{-}$
23	22	eqcomd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to \underset{˙}{-} = d$
24	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to x \underset{˙}{-} y = x d y$
25	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to a \underset{˙}{-} b = a d b$
26	24 25	eqeq12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (x \underset{˙}{-} y = a \underset{˙}{-} b \leftrightarrow x d y = a d b)$
27	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to y \underset{˙}{-} z = y d z$
28	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to b \underset{˙}{-} c = b d c$
29	27 28	eqeq12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (y \underset{˙}{-} z = b \underset{˙}{-} c \leftrightarrow y d z = b d c)$
30	26 29	anbi12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \leftrightarrow (x d y = a d b \land y d z = b d c))$
31	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to x \underset{˙}{-} u = x d u$
32	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to a \underset{˙}{-} v = a d v$
33	31 32	eqeq12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (x \underset{˙}{-} u = a \underset{˙}{-} v \leftrightarrow x d u = a d v)$
34	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to y \underset{˙}{-} u = y d u$
35	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to b \underset{˙}{-} v = b d v$
36	34 35	eqeq12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (y \underset{˙}{-} u = b \underset{˙}{-} v \leftrightarrow y d u = b d v)$
37	33 36	anbi12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to ((x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v) \leftrightarrow (x d u = a d v \land y d u = b d v))$
38	30 37	anbi12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (((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)) \leftrightarrow ((x d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v)))$
39	20 38	anbi12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (((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))) \leftrightarrow ((x \neq y \land y \in (x i z) \land b \in (a i c)) \land ((x d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))))$
40	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to z \underset{˙}{-} u = z d u$
41	23	oveqd	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to c \underset{˙}{-} v = c d v$
42	40 41	eqeq12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to (z \underset{˙}{-} u = c \underset{˙}{-} v \leftrightarrow z d u = c d v)$
43	39 42	imbi12d	$⊢ (((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \land v \in P) \to ((((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) \leftrightarrow (((x \neq y \land y \in (x i z) \land b \in (a i c)) \land ((x d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
44	12 43	raleqbidva	$⊢ ((((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \land c \in P) \to (\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) \leftrightarrow \forall v \in p (((x \neq y \land y \in (x i z) \land b \in (a i c)) \land ((x d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
45	11 44	raleqbidva	$⊢ (((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \land b \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
46	10 45	raleqbidva	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land a \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
47	9 46	raleqbidva	$⊢ (((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
48	8 47	raleqbidva	$⊢ ((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land z \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
49	7 48	raleqbidva	$⊢ (((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
50	6 49	raleqbidva	$⊢ ((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \to (\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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
51	5 50	raleqbidva	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \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) \leftrightarrow \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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d v))$
52	7	adantr	$⊢ ((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \to P = p$
53	52	adantr	$⊢ (((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \to P = p$
54	13	ad3antrrr	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to i = I$
55	54	eqcomd	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to I = i$
56	55	oveqd	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to x I z = x i z$
57	56	eleq2d	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to (y \in (x I z) \leftrightarrow y \in (x i z))$
58	21	ad3antrrr	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to d = \underset{˙}{-}$
59	58	eqcomd	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to \underset{˙}{-} = d$
60	59	oveqd	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to y \underset{˙}{-} z = y d z$
61	59	oveqd	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to a \underset{˙}{-} b = a d b$
62	60 61	eqeq12d	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to (y \underset{˙}{-} z = a \underset{˙}{-} b \leftrightarrow y d z = a d b)$
63	57 62	anbi12d	$⊢ ((((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \land z \in P) \to ((y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow (y \in (x i z) \land y d z = a d b))$
64	53 63	rexeqbidva	$⊢ (((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \land b \in P) \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 d z = a d b))$
65	52 64	raleqbidva	$⊢ ((((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \in P) \land a \in P) \to (\forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b) \leftrightarrow \forall b \in p \exists z \in p (y \in (x i z) \land y d z = a d b))$
66	7 65	raleqbidva	$⊢ (((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \land y \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) \leftrightarrow \forall a \in p \forall b \in p \exists z \in p (y \in (x i z) \land y d z = a d b))$
67	6 66	raleqbidva	$⊢ ((p = P \land d = \underset{˙}{-} \land i = I) \land x \in P) \to (\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) \leftrightarrow \forall y \in p \forall a \in p \forall b \in p \exists z \in p (y \in (x i z) \land y d z = a d b))$
68	5 67	raleqbidva	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \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) \leftrightarrow \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 d z = a d b))$
69	51 68	anbi12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \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)) \leftrightarrow (\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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d 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 d z = a d b)))$
70	1 2 3 69	sbcie3s	$⊢ f = G \to (\underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d 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 d z = a d b)) \leftrightarrow (\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)))$
71		df-trkgcb	$⊢ 𝒢_{Tarski}^{CB} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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 d y = a d b \land y d z = b d c) \land (x d u = a d v \land y d u = b d v))) \to z d u = c d 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 d z = a d b))\}$
72	70 71	elab4g	$⊢ 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)))$

Metamath Proof Explorer

Theorem istrkgcb

Proof