Metamath Proof Explorer

Theorem btwnxfr

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion btwnxfr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF→EBtwnDF

Proof

Step Hyp Ref Expression
1 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF↔ABCgrDE∧ACCgrDF∧BCCgrEF
2 simp2 ⊢ABCgrDE∧ACCgrDF∧BCCgrEF→ACCgrDF
3 1 2 syl6bi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF→ACCgrDF
4 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→N∈ℕ
5 simp21 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→A∈𝔼⁡N
6 simp22 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→B∈𝔼⁡N
7 simp23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→C∈𝔼⁡N
8 simp31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→D∈𝔼⁡N
9 simp33 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→F∈𝔼⁡N
10 cgrxfr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ACCgrDF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
11 4 5 6 7 8 9 10 syl132anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ACCgrDF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
12 3 11 sylan2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
13 12 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF
14 simprrl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→eBtwnDF
15 14 14 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→eBtwnDF∧eBtwnDF
16 simpl1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→N∈ℕ
17 simpl31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→D∈𝔼⁡N
18 simpl33 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→F∈𝔼⁡N
19 16 17 18 cgrrflxd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DFCgrDF
20 simpr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→e∈𝔼⁡N
21 16 20 18 cgrrflxd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→eFCgreF
22 19 21 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DFCgrDF∧eFCgreF
23 22 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→DFCgrDF∧eFCgreF
24 simpr ⊢BBtwnAC∧ABCCgr3DEF→ABCCgr3DEF
25 simpr ⊢eBtwnDF∧ABCCgr3DeF→ABCCgr3DeF
26 simpl2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
27 simpl3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N
28 17 20 18 3jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N
29 cgr3tr4 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N→ABCCgr3DEF∧ABCCgr3DeF→DEFCgr3DeF
30 16 26 27 28 29 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→ABCCgr3DEF∧ABCCgr3DeF→DEFCgr3DeF
31 cgr3com ⊢N∈ℕ∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N→DEFCgr3DeF↔DeFCgr3DEF
32 16 27 17 20 18 31 syl113anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DEFCgr3DeF↔DeFCgr3DEF
33 simpl32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→E∈𝔼⁡N
34 brcgr3 ⊢N∈ℕ∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→DeFCgr3DEF↔DeCgrDE∧DFCgrDF∧eFCgrEF
35 16 17 20 18 17 33 18 34 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DeFCgr3DEF↔DeCgrDE∧DFCgrDF∧eFCgrEF
36 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧DeCgrDE∧DFCgrDF∧eFCgrEF→DeCgrDE
37 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧DeCgrDE∧DFCgrDF∧eFCgrEF→eFCgrEF
38 16 20 18 33 18 37 cgrcomlrand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧DeCgrDE∧DFCgrDF∧eFCgrEF→FeCgrFE
39 36 38 jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧DeCgrDE∧DFCgrDF∧eFCgrEF→DeCgrDE∧FeCgrFE
40 39 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DeCgrDE∧DFCgrDF∧eFCgrEF→DeCgrDE∧FeCgrFE
41 35 40 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DeFCgr3DEF→DeCgrDE∧FeCgrFE
42 32 41 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→DEFCgr3DeF→DeCgrDE∧FeCgrFE
43 30 42 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→ABCCgr3DEF∧ABCCgr3DeF→DeCgrDE∧FeCgrFE
44 24 25 43 syl2ani ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→DeCgrDE∧FeCgrFE
45 44 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→DeCgrDE∧FeCgrFE
46 15 23 45 3jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→eBtwnDF∧eBtwnDF∧DFCgrDF∧eFCgreF∧DeCgrDE∧FeCgrFE
47 46 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→eBtwnDF∧eBtwnDF∧DFCgrDF∧eFCgreF∧DeCgrDE∧FeCgrFE
48 brifs ⊢N∈ℕ∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N→DeFeInnerFiveSegDeFE↔eBtwnDF∧eBtwnDF∧DFCgrDF∧eFCgreF∧DeCgrDE∧FeCgrFE
49 ifscgr ⊢N∈ℕ∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N→DeFeInnerFiveSegDeFE→eeCgreE
50 48 49 sylbird ⊢N∈ℕ∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧D∈𝔼⁡N∧e∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N→eBtwnDF∧eBtwnDF∧DFCgrDF∧eFCgreF∧DeCgrDE∧FeCgrFE→eeCgreE
51 16 17 20 18 20 17 20 18 33 50 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→eBtwnDF∧eBtwnDF∧DFCgrDF∧eFCgreF∧DeCgrDE∧FeCgrFE→eeCgreE
52 47 51 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→eeCgreE
53 cgrid2 ⊢N∈ℕ∧e∈𝔼⁡N∧e∈𝔼⁡N∧E∈𝔼⁡N→eeCgreE→e=E
54 16 20 20 33 53 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→eeCgreE→e=E
55 52 54 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→e=E
56 55 imp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→e=E
57 56 14 eqbrtrrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧eBtwnDF∧ABCCgr3DeF→EBtwnDF
58 57 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧e∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF→eBtwnDF∧ABCCgr3DeF→EBtwnDF
59 58 an32s ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF∧e∈𝔼⁡N→eBtwnDF∧ABCCgr3DeF→EBtwnDF
60 59 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF→∃e∈𝔼⁡NeBtwnDF∧ABCCgr3DeF→EBtwnDF
61 13 60 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧BBtwnAC∧ABCCgr3DEF→EBtwnDF
62 61 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N→BBtwnAC∧ABCCgr3DEF→EBtwnDF