Theorem istrkgc

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

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

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$$⊢P={\mathrm{Base}}_G$$
2		istrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		istrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		simpl	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to p=P$$
5		simpr	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to d=\underset{\dot{}}{-}$$
6	5	oveqd	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to xdy=x\underset{\dot{}}{-}y$$
7	5	oveqd	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to ydx=y\underset{\dot{}}{-}x$$
8	6 7	eqeq12d	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(xdy=ydx\leftrightarrow x\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\right)$$
9	4 8	raleqbidv	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\forall y\in pxdy=ydx\leftrightarrow \forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\right)$$
10	4 9	raleqbidv	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\forall x\in p\forall y\in pxdy=ydx\leftrightarrow \forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\right)$$
11	5	oveqd	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to zdz=z\underset{\dot{}}{-}z$$
12	6 11	eqeq12d	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(xdy=zdz\leftrightarrow x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\right)$$
13	12	imbi1d	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\left(xdy=zdz\to x=y\right)\leftrightarrow \left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)$$
14	4 13	raleqbidv	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\forall z\in p\left(xdy=zdz\to x=y\right)\leftrightarrow \forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)$$
15	4 14	raleqbidv	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\forall y\in p\forall z\in p\left(xdy=zdz\to x=y\right)\leftrightarrow \forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)$$
16	4 15	raleqbidv	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\forall x\in p\forall y\in p\forall z\in p\left(xdy=zdz\to x=y\right)\leftrightarrow \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)$$
17	10 16	anbi12d	$$⊢\left(p=P\wedge d=\underset{\dot{}}{-}\right)\to \left(\left(\forall x\in p\forall y\in pxdy=ydx\wedge \forall x\in p\forall y\in p\forall z\in p\left(xdy=zdz\to x=y\right)\right)\leftrightarrow \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\wedge \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)\right)$$
18	1 2 17	sbcie2s	$$⊢f=G\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(f\right)/d\underset{\dot{}}{]}\left(\forall x\in p\forall y\in pxdy=ydx\wedge \forall x\in p\forall y\in p\forall z\in p\left(xdy=zdz\to x=y\right)\right)\leftrightarrow \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\wedge \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)\right)$$
19		df-trkgc	$$⊢{𝒢}_{\mathrm{Tarski}}^C=\left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(f\right)/d\underset{\dot{}}{]}\left(\forall x\in p\forall y\in pxdy=ydx\wedge \forall x\in p\forall y\in p\forall z\in p\left(xdy=zdz\to x=y\right)\right)\right\}$$
20	18 19	elab4g	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^C\leftrightarrow \left(G\in \mathrm{V}\wedge \left(\forall x\in P\forall y\in Px\underset{\dot{}}{-}y=y\underset{\dot{}}{-}x\wedge \forall x\in P\forall y\in P\forall z\in P\left(x\underset{\dot{}}{-}y=z\underset{\dot{}}{-}z\to x=y\right)\right)\right)$$