Metamath Proof Explorer

Theorem fscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion fscgr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDFiveSegEFGH∧A≠B→CDCgrGH

Proof

Step Hyp Ref Expression
1 brfs ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDFiveSegEFGH↔AColinearBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH
2 1 anbi1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDFiveSegEFGH∧A≠B↔AColinearBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B
3 simp11 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→N∈ℕ
4 simp12 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→A∈𝔼⁡N
5 simp13 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→B∈𝔼⁡N
6 simp21 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→C∈𝔼⁡N
7 brcolinear ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
8 3 4 5 6 7 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
9 simp23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→E∈𝔼⁡N
10 simp31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→F∈𝔼⁡N
11 simp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→G∈𝔼⁡N
12 cgr3permute2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N→ABCCgr3EFG↔BACCgr3FEG
13 3 4 5 6 9 10 11 12 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCCgr3EFG↔BACCgr3FEG
14 ancom ⊢ADCgrEH∧BDCgrFH↔BDCgrFH∧ADCgrEH
15 14 a1i ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ADCgrEH∧BDCgrFH↔BDCgrFH∧ADCgrEH
16 13 15 3anbi23d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔ABtwnBC∧BACCgr3FEG∧BDCgrFH∧ADCgrEH
17 simp22 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→D∈𝔼⁡N
18 simp33 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→H∈𝔼⁡N
19 brofs2 ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BACDOuterFiveSegFEGH↔ABtwnBC∧BACCgr3FEG∧BDCgrFH∧ADCgrEH
20 3 5 4 6 17 10 9 11 18 19 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BACDOuterFiveSegFEGH↔ABtwnBC∧BACCgr3FEG∧BDCgrFH∧ADCgrEH
21 16 20 bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔BACDOuterFiveSegFEGH
22 necom ⊢A≠B↔B≠A
23 22 a1i ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→A≠B↔B≠A
24 21 23 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B↔BACDOuterFiveSegFEGH∧B≠A
25 5segofs ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧F∈𝔼⁡N∧E∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BACDOuterFiveSegFEGH∧B≠A→CDCgrGH
26 3 5 4 6 17 10 9 11 18 25 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BACDOuterFiveSegFEGH∧B≠A→CDCgrGH
27 24 26 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B→CDCgrGH
28 27 expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
29 28 3expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC→ABCCgr3EFG→ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
30 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BBtwnCA↔BBtwnAC
31 3 5 6 4 30 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA↔BBtwnAC
32 31 3anbi1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔BBtwnAC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH
33 brofs2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDOuterFiveSegEFGH↔BBtwnAC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH
34 32 33 bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔ABCDOuterFiveSegEFGH
35 34 anbi1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B↔ABCDOuterFiveSegEFGH∧A≠B
36 5segofs ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDOuterFiveSegEFGH∧A≠B→CDCgrGH
37 35 36 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B→CDCgrGH
38 37 expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
39 38 3expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→BBtwnCA→ABCCgr3EFG→ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
40 cgr3permute1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N→ABCCgr3EFG↔ACBCgr3EGF
41 3 4 5 6 9 10 11 40 syl133anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCCgr3EFG↔ACBCgr3EGF
42 41 3anbi2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→CBtwnAB∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔CBtwnAB∧ACBCgr3EGF∧ADCgrEH∧BDCgrFH
43 brifs2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧G∈𝔼⁡N∧F∈𝔼⁡N∧H∈𝔼⁡N→ACBDInnerFiveSegEGFH↔CBtwnAB∧ACBCgr3EGF∧ADCgrEH∧BDCgrFH
44 3 4 6 5 17 9 11 10 18 43 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ACBDInnerFiveSegEGFH↔CBtwnAB∧ACBCgr3EGF∧ADCgrEH∧BDCgrFH
45 42 44 bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→CBtwnAB∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH↔ACBDInnerFiveSegEGFH
46 ifscgr ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧G∈𝔼⁡N∧F∈𝔼⁡N∧H∈𝔼⁡N→ACBDInnerFiveSegEGFH→CDCgrGH
47 3 4 6 5 17 9 11 10 18 46 syl333anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ACBDInnerFiveSegEGFH→CDCgrGH
48 45 47 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→CBtwnAB∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH→CDCgrGH
49 48 a1dd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→CBtwnAB∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
50 49 3expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→CBtwnAB→ABCCgr3EFG→ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
51 29 39 50 3jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB→ABCCgr3EFG→ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
52 8 51 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→AColinearBC→ABCCgr3EFG→ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
53 52 3impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→AColinearBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH→A≠B→CDCgrGH
54 53 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→AColinearBC∧ABCCgr3EFG∧ADCgrEH∧BDCgrFH∧A≠B→CDCgrGH
55 2 54 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N∧F∈𝔼⁡N∧G∈𝔼⁡N∧H∈𝔼⁡N→ABCDFiveSegEFGH∧A≠B→CDCgrGH