Metamath Proof Explorer

Theorem idinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion idinside ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
4 cgrid2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
5 1 2 2 3 4 syl13anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
6 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
7 axbtwnid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝐶 = 𝐴 ) )
8 1 2 6 7 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝐶 = 𝐴 ) )
9 opeq1 ⊢ ( 𝐶 = 𝐴 → ⟨ 𝐶 , 𝐶 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
10 opeq1 ⊢ ( 𝐶 = 𝐴 → ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ )
11 9 10 breq12d ⊢ ( 𝐶 = 𝐴 → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ) )
12 11 imbi1d ⊢ ( 𝐶 = 𝐴 → ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) )
13 12 biimpcd ⊢ ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) → ( 𝐶 = 𝐴 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) )
14 ax-1 ⊢ ( 𝐶 = 𝐷 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
15 13 14 syl8 ⊢ ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) → ( 𝐶 = 𝐴 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) ) )
16 5 8 15 sylsyld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) ) )
17 16 3impd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
18 opeq2 ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐴 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
19 18 breq2d ⊢ ( 𝐴 = 𝐵 → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
20 19 3anbi1d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
21 20 imbi1d ⊢ ( 𝐴 = 𝐵 → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ↔ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
22 17 21 imbitrid ⊢ ( 𝐴 = 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
23 simpr1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
24 simpr2l ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
25 simpr2r ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
26 simpr3l ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
27 btwncolinear1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
28 23 24 25 26 27 syl13anc ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
29 idd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ) )
30 idd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
31 28 29 30 3anim123d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
32 simp1 ⊢ ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ )
33 32 anim2i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
34 3simpc ⊢ ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
35 34 adantl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
36 33 35 jca ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
37 lineid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐶 = 𝐷 ) )
38 36 37 syl5 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐶 = 𝐷 ) )
39 38 expd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
40 39 impcom ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
41 31 40 syld ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
42 41 ex ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
43 22 42 pm2.61ine ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )