istrkgcb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > istrkgcb		Structured version Visualization version GIF version

Theorem istrkgcb 28918

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

**Hypotheses**
Ref	Expression
istrkg.p	⊢ 𝑃 = (Base‘𝐺)
istrkg.d	⊢ − = (dist‘𝐺)
istrkg.i	⊢ 𝐼 = (Itv‘𝐺)

**Assertion**
Ref	Expression
istrkgcb	⊢ (𝐺 ∈ TarskiG_CB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))

Distinct variable groups: 𝑎,𝑏,𝑐,𝑢,𝑣,𝑥,𝑦,𝑧,𝐼 𝑃,𝑎,𝑏,𝑐,𝑢,𝑣,𝑥,𝑦,𝑧 − ,𝑎,𝑏,𝑐,𝑢,𝑣,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐺(𝑥, 𝑦, 𝑧, 𝑣, 𝑢, 𝑎, 𝑏, 𝑐)

Proof of Theorem istrkgcb Dummy variables 𝑓 𝑑 𝑖 𝑝 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 [wsbc 3738 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 distcds 17437 TarskiG_CBcstrkgcb 28892 Itvcitv 28895

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-nul 5259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-iota 6494 df-fv 6546 df-ov 7423 df-trkgcb 28912

This theorem is used by: axtgsegcon 28926 axtg5seg 28927 f1otrg 29448 eengtrkg 29564

W3C validator