Metamath Proof Explorer

Theorem linecgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (Contributed by Scott Fenton, 6-Oct-2013)

Ref Expression
Assertion linecgr ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simprlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ )
2 cgr3rflx ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )
3 2 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )
4 3 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ )
5 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) )
6 1 4 5 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) )
7 simprll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → 𝐴 ≠ 𝐵 )
8 6 7 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) )
9 8 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) ) )
10 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
11 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simp22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simp23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
15 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
16 brfs ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑃 ⟩ ⟩ FiveSeg ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑄 ⟩ ⟩ ↔ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ) )
17 16 anbi1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑃 ⟩ ⟩ FiveSeg ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑄 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) ) )
18 fscgr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑃 ⟩ ⟩ FiveSeg ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝑄 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
19 17 18 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
20 10 11 12 13 14 11 12 13 15 19 syl333anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )
21 9 20 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝑃 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ∧ ⟨ 𝐵 , 𝑃 ⟩ Cgr ⟨ 𝐵 , 𝑄 ⟩ ) ) → ⟨ 𝐶 , 𝑃 ⟩ Cgr ⟨ 𝐶 , 𝑄 ⟩ ) )