Metamath Proof Explorer

Theorem ofscom

Description: The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013)

Ref Expression
Assertion ofscom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A B C D OuterFiveSeg E F G H ↔ E F G H OuterFiveSeg A B C D

Proof

Step Hyp Ref Expression
1 ancom ⊢ B Btwn A C ∧ F Btwn E G ↔ F Btwn E G ∧ B Btwn A C
2 1 a1i ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → B Btwn A C ∧ F Btwn E G ↔ F Btwn E G ∧ B Btwn A C
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 simp23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N
7 simp31 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N
8 cgrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B Cgr E F ↔ E F Cgr A B
9 3 4 5 6 7 8 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A B Cgr E F ↔ E F Cgr A B
10 simp21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
11 simp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → G ∈ 𝔼 ⁡ N
12 cgrcom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N → B C Cgr F G ↔ F G Cgr B C
13 3 5 10 7 11 12 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → B C Cgr F G ↔ F G Cgr B C
14 9 13 anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A B Cgr E F ∧ B C Cgr F G ↔ E F Cgr A B ∧ F G Cgr B C
15 simp22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
16 simp33 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → H ∈ 𝔼 ⁡ N
17 cgrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A D Cgr E H ↔ E H Cgr A D
18 3 4 15 6 16 17 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A D Cgr E H ↔ E H Cgr A D
19 cgrcom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → B D Cgr F H ↔ F H Cgr B D
20 3 5 15 7 16 19 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → B D Cgr F H ↔ F H Cgr B D
21 18 20 anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A D Cgr E H ∧ B D Cgr F H ↔ E H Cgr A D ∧ F H Cgr B D
22 2 14 21 3anbi123d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → B Btwn A C ∧ F Btwn E G ∧ A B Cgr E F ∧ B C Cgr F G ∧ A D Cgr E H ∧ B D Cgr F H ↔ F Btwn E G ∧ B Btwn A C ∧ E F Cgr A B ∧ F G Cgr B C ∧ E H Cgr A D ∧ F H Cgr B D
23 brofs ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A B C D OuterFiveSeg E F G H ↔ B Btwn A C ∧ F Btwn E G ∧ A B Cgr E F ∧ B C Cgr F G ∧ A D Cgr E H ∧ B D Cgr F H
24 brofs ⊢ N ∈ ℕ ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → E F G H OuterFiveSeg A B C D ↔ F Btwn E G ∧ B Btwn A C ∧ E F Cgr A B ∧ F G Cgr B C ∧ E H Cgr A D ∧ F H Cgr B D
25 3 6 7 11 16 4 5 10 15 24 syl333anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → E F G H OuterFiveSeg A B C D ↔ F Btwn E G ∧ B Btwn A C ∧ E F Cgr A B ∧ F G Cgr B C ∧ E H Cgr A D ∧ F H Cgr B D
26 22 23 25 3bitr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ G ∈ 𝔼 ⁡ N ∧ H ∈ 𝔼 ⁡ N → A B C D OuterFiveSeg E F G H ↔ E F G H OuterFiveSeg A B C D