Metamath Proof Explorer

Theorem colinearxfr

Description: Transfer law for colinearity. Theorem 4.13 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearxfr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BColinearAC∧ABCCgr3DEF→EColinearDF

Proof

Step Hyp Ref Expression
1 btwnxfr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF→EBtwnDF
2 1 expcomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF→BBtwnAC→EBtwnDF
3 2 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→BBtwnAC→EBtwnDF
4 cgr3permute4 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔CABCgr3FDE
5 biid ⊢N∈ℕ↔N∈ℕ
6 3anrot ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
7 3anrot ⊢F∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N↔D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N
8 btwnxfr ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→ABtwnCB∧CABCgr3FDE→DBtwnFE
9 5 6 7 8 syl3anbr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABtwnCB∧CABCgr3FDE→DBtwnFE
10 9 expcomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→CABCgr3FDE→ABtwnCB→DBtwnFE
11 4 10 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF→ABtwnCB→DBtwnFE
12 11 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→ABtwnCB→DBtwnFE
13 cgr3permute3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔BCACgr3EFD
14 3anrot ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
15 3anrot ⊢D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N↔E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N
16 btwnxfr ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N→CBtwnBA∧BCACgr3EFD→FBtwnED
17 5 14 15 16 syl3anb ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→CBtwnBA∧BCACgr3EFD→FBtwnED
18 17 expcomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BCACgr3EFD→CBtwnBA→FBtwnED
19 13 18 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF→CBtwnBA→FBtwnED
20 19 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→CBtwnBA→FBtwnED
21 3 12 20 3orim123d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→BBtwnAC∨ABtwnCB∨CBtwnBA→EBtwnDF∨DBtwnFE∨FBtwnED
22 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→N∈ℕ
23 simp22 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→B∈𝔼⁡N
24 simp21 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→A∈𝔼⁡N
25 simp23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→C∈𝔼⁡N
26 brcolinear ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→BColinearAC↔BBtwnAC∨ABtwnCB∨CBtwnBA
27 22 23 24 25 26 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BColinearAC↔BBtwnAC∨ABtwnCB∨CBtwnBA
28 27 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→BColinearAC↔BBtwnAC∨ABtwnCB∨CBtwnBA
29 simp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→E∈𝔼⁡N
30 simp31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→D∈𝔼⁡N
31 simp33 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→F∈𝔼⁡N
32 brcolinear ⊢N∈ℕ∧E∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N→EColinearDF↔EBtwnDF∨DBtwnFE∨FBtwnED
33 22 29 30 31 32 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→EColinearDF↔EBtwnDF∨DBtwnFE∨FBtwnED
34 33 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→EColinearDF↔EBtwnDF∨DBtwnFE∨FBtwnED
35 21 28 34 3imtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧ABCCgr3DEF→BColinearAC→EColinearDF
36 35 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF→BColinearAC→EColinearDF
37 36 com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BColinearAC→ABCCgr3DEF→EColinearDF
38 37 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BColinearAC∧ABCCgr3DEF→EColinearDF