Metamath Proof Explorer

Theorem istrkgcb

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

Ref Expression
Hypotheses istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
istrkg.d ⊢ − = ( dist ‘ 𝐺 )
istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion istrkgcb ( 𝐺 ∈ TarskiGCB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 istrkg.d ⊢ − = ( dist ‘ 𝐺 )
3 istrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 simp1 ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5 4 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
6 5 adantr ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
7 6 adantr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑃 = 𝑝 )
8 7 adantr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 = 𝑝 )
9 8 adantr ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → 𝑃 = 𝑝 )
10 9 adantr ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → 𝑃 = 𝑝 )
11 5 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑃 = 𝑝 )
12 6 ad6antr ⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → 𝑃 = 𝑝 )
13 simpll3 ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑖 = 𝐼 )
14 13 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑖 = 𝐼 )
15 14 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝐼 = 𝑖 )
16 15 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
17 16 eleq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
18 15 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑎 𝐼 𝑐 ) = ( 𝑎 𝑖 𝑐 ) )
19 18 eleq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ↔ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) )
20 17 19 3anbi23d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ↔ ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ) )
21 simpll2 ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑑 = − )
22 21 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑑 = − )
23 22 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → − = 𝑑 )
24 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 𝑑 𝑦 ) )
25 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑎 − 𝑏 ) = ( 𝑎 𝑑 𝑏 ) )
26 24 25 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ↔ ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ) )
27 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑦 − 𝑧 ) = ( 𝑦 𝑑 𝑧 ) )
28 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑏 − 𝑐 ) = ( 𝑏 𝑑 𝑐 ) )
29 27 28 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ↔ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) )
30 26 29 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ↔ ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ) )
31 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑥 − 𝑢 ) = ( 𝑥 𝑑 𝑢 ) )
32 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑎 − 𝑣 ) = ( 𝑎 𝑑 𝑣 ) )
33 31 32 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ↔ ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ) )
34 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑦 − 𝑢 ) = ( 𝑦 𝑑 𝑢 ) )
35 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑏 − 𝑣 ) = ( 𝑏 𝑑 𝑣 ) )
36 34 35 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ↔ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) )
37 33 36 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ↔ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) )
38 30 37 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ↔ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) )
39 20 38 anbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) ↔ ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) ) )
40 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑧 − 𝑢 ) = ( 𝑧 𝑑 𝑢 ) )
41 23 oveqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑐 − 𝑣 ) = ( 𝑐 𝑑 𝑣 ) )
42 40 41 eqeq12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ↔ ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) )
43 39 42 imbi12d ⊢ ( ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
44 12 43 raleqbidva ⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
45 11 44 raleqbidva ⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
46 10 45 raleqbidva ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
47 9 46 raleqbidva ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
48 8 47 raleqbidva ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
49 7 48 raleqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
50 6 49 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
51 5 50 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ) )
52 7 adantr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → 𝑃 = 𝑝 )
53 52 adantr ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑃 = 𝑝 )
54 13 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑖 = 𝐼 )
55 54 eqcomd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝐼 = 𝑖 )
56 55 oveqd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑧 ) = ( 𝑥 𝑖 𝑧 ) )
57 56 eleq2d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
58 21 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑑 = − )
59 58 eqcomd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → − = 𝑑 )
60 59 oveqd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑦 − 𝑧 ) = ( 𝑦 𝑑 𝑧 ) )
61 59 oveqd ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑎 − 𝑏 ) = ( 𝑎 𝑑 𝑏 ) )
62 60 61 eqeq12d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ↔ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) )
63 57 62 anbi12d ⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
64 53 63 rexeqbidva ⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
65 52 64 raleqbidva ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
66 7 65 raleqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
67 6 66 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
68 5 67 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) )
69 51 68 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) ) )
70 1 2 3 69 sbcie3s ⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ) ) )
71 df-trkgcb ⊢ TarskiGCB = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∀ 𝑐 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑎 𝑑 𝑏 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑏 𝑑 𝑐 ) ) ∧ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑎 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑏 𝑑 𝑣 ) ) ) ) → ( 𝑧 𝑑 𝑢 ) = ( 𝑐 𝑑 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑎 ∈ 𝑝 ∀ 𝑏 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ∧ ( 𝑦 𝑑 𝑧 ) = ( 𝑎 𝑑 𝑏 ) ) ) }
72 70 71 elab4g ⊢ ( 𝐺 ∈ TarskiGCB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( ( 𝑥 ≠ 𝑦 ∧ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑏 ∈ ( 𝑎 𝐼 𝑐 ) ) ∧ ( ( ( 𝑥 − 𝑦 ) = ( 𝑎 − 𝑏 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑏 − 𝑐 ) ) ∧ ( ( 𝑥 − 𝑢 ) = ( 𝑎 − 𝑣 ) ∧ ( 𝑦 − 𝑢 ) = ( 𝑏 − 𝑣 ) ) ) ) → ( 𝑧 − 𝑢 ) = ( 𝑐 − 𝑣 ) ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑎 − 𝑏 ) ) ) ) )