Step |
Hyp |
Ref |
Expression |
1 |
|
dfcgra2.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
dfcgra2.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
3 |
|
dfcgra2.m |
⊢ − = ( dist ‘ 𝐺 ) |
4 |
|
dfcgra2.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
5 |
|
dfcgra2.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
6 |
|
dfcgra2.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) |
7 |
|
dfcgra2.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) |
8 |
|
dfcgra2.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) |
9 |
|
dfcgra2.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) |
10 |
|
dfcgra2.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) |
11 |
|
eqid |
⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 ) |
12 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐺 ∈ TarskiG ) |
13 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐴 ∈ 𝑃 ) |
14 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐵 ∈ 𝑃 ) |
15 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐶 ∈ 𝑃 ) |
16 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐷 ∈ 𝑃 ) |
17 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐸 ∈ 𝑃 ) |
18 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐹 ∈ 𝑃 ) |
19 |
|
simpr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
20 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane1 |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐴 ≠ 𝐵 ) |
21 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane2 |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐵 ≠ 𝐶 ) |
22 |
21
|
necomd |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐶 ≠ 𝐵 ) |
23 |
20 22
|
jca |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ) |
24 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane3 |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐸 ≠ 𝐷 ) |
25 |
24
|
necomd |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐷 ≠ 𝐸 ) |
26 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane4 |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐸 ≠ 𝐹 ) |
27 |
26
|
necomd |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → 𝐹 ≠ 𝐸 ) |
28 |
25 27
|
jca |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) |
29 |
|
simprl |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) |
30 |
|
simprr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) |
31 |
4
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐺 ∈ TarskiG ) |
32 |
|
simp-5r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ∈ 𝑃 ) |
33 |
6
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ∈ 𝑃 ) |
34 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ∈ 𝑃 ) |
35 |
|
simpllr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑑 ∈ 𝑃 ) |
36 |
9
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ∈ 𝑃 ) |
37 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑓 ∈ 𝑃 ) |
38 |
10
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ∈ 𝑃 ) |
39 |
8
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ∈ 𝑃 ) |
40 |
7
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ 𝑃 ) |
41 |
5
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ 𝑃 ) |
42 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
43 |
1 2 31 11 41 33 40 39 36 38 42
|
cgracom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐴 𝐵 𝐶 ”〉 ) |
44 |
29
|
simplld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ) |
45 |
20
|
ad5antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ≠ 𝐵 ) |
46 |
1 3 2 31 33 41 32 44 45
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ≠ 𝑎 ) |
47 |
1 2 11 33 32 41 31 41 44 46 45
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 ) |
48 |
1 2 11 41 32 33 31 47
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 ) |
49 |
1 2 11 31 39 36 38 41 33 40 43 32 48
|
cgrahl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑎 𝐵 𝐶 ”〉 ) |
50 |
29
|
simprld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ) |
51 |
22
|
ad5antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ≠ 𝐵 ) |
52 |
1 3 2 31 33 40 34 50 51
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ≠ 𝑐 ) |
53 |
1 2 11 33 34 40 31 41 50 52 51
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 ) |
54 |
1 2 11 40 34 33 31 53
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 ) |
55 |
1 2 11 31 39 36 38 32 33 40 49 34 54
|
cgrahl2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑎 𝐵 𝑐 ”〉 ) |
56 |
1 2 31 11 39 36 38 32 33 34 55
|
cgracom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝑎 𝐵 𝑐 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
57 |
30
|
simplld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ) |
58 |
25
|
ad5antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ≠ 𝐸 ) |
59 |
1 3 2 31 36 39 35 57 58
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ≠ 𝑑 ) |
60 |
1 2 11 36 35 39 31 41 57 59 58
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑑 ) |
61 |
1 2 11 39 35 36 31 60
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ) |
62 |
1 2 11 31 32 33 34 39 36 38 56 35 61
|
cgrahl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝑎 𝐵 𝑐 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑑 𝐸 𝐹 ”〉 ) |
63 |
30
|
simprld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ) |
64 |
27
|
ad5antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ≠ 𝐸 ) |
65 |
1 3 2 31 36 38 37 63 64
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ≠ 𝑓 ) |
66 |
1 2 11 36 37 38 31 41 63 65 64
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑓 ) |
67 |
1 2 11 38 37 36 31 66
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) |
68 |
1 2 11 31 32 33 34 35 36 38 62 37 67
|
cgrahl2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 〈“ 𝑎 𝐵 𝑐 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑑 𝐸 𝑓 ”〉 ) |
69 |
46
|
necomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ≠ 𝐵 ) |
70 |
1 2 11 32 41 33 31 69
|
hlid |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 ) |
71 |
52
|
necomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ≠ 𝐵 ) |
72 |
1 2 11 34 41 33 31 71
|
hlid |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 ) |
73 |
1 3 2 31 33 41 32 44
|
tgbtwncom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝑎 𝐼 𝐵 ) ) |
74 |
29
|
simplrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) |
75 |
1 3 2 31 41 32 36 39 74
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝐴 ) = ( 𝐸 − 𝐷 ) ) |
76 |
30
|
simplrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) |
77 |
76
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝑑 ) ) |
78 |
1 3 2 31 33 41 39 35 77
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝑑 ) ) |
79 |
1 3 2 31 32 41 33 36 39 35 73 57 75 78
|
tgcgrextend |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝐵 ) = ( 𝐸 − 𝑑 ) ) |
80 |
1 3 2 31 32 33 36 35 79
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝑎 ) = ( 𝐸 − 𝑑 ) ) |
81 |
1 3 2 31 33 40 34 50
|
tgbtwncom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝑐 𝐼 𝐵 ) ) |
82 |
29
|
simprrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) |
83 |
1 3 2 31 40 34 36 38 82
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑐 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) |
84 |
30
|
simprrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) |
85 |
84
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝑓 ) ) |
86 |
1 3 2 31 33 40 38 37 85
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝑓 ) ) |
87 |
1 3 2 31 34 40 33 36 38 37 81 63 83 86
|
tgcgrextend |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑐 − 𝐵 ) = ( 𝐸 − 𝑓 ) ) |
88 |
1 3 2 31 34 33 36 37 87
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝑐 ) = ( 𝐸 − 𝑓 ) ) |
89 |
1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88
|
cgracgr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) |
90 |
29 30 89
|
3jca |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) |
91 |
90
|
ex |
⊢ ( ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
92 |
91
|
reximdva |
⊢ ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) → ( ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
93 |
92
|
reximdva |
⊢ ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
94 |
93
|
imp |
⊢ ( ( ( ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) |
95 |
1 3 2 4 6 5 9 8
|
axtgsegcon |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ) |
96 |
1 3 2 4 6 7 9 10
|
axtgsegcon |
⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) |
97 |
|
reeanv |
⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ∃ 𝑐 ∈ 𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) |
98 |
95 96 97
|
sylanbrc |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) |
99 |
1 3 2 4 9 8 6 5
|
axtgsegcon |
⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) |
100 |
1 3 2 4 9 10 6 7
|
axtgsegcon |
⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) |
101 |
|
reeanv |
⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ∃ 𝑑 ∈ 𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ∃ 𝑓 ∈ 𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) |
102 |
99 100 101
|
sylanbrc |
⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) |
103 |
98 102
|
jca |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
104 |
|
r19.41vv |
⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ) |
105 |
|
ancom |
⊢ ( ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
106 |
105
|
2rexbii |
⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
107 |
|
ancom |
⊢ ( ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
108 |
104 106 107
|
3bitr3i |
⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
109 |
108
|
2rexbii |
⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
110 |
|
r19.41vv |
⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
111 |
109 110
|
bitr2i |
⊢ ( ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
112 |
103 111
|
sylib |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
113 |
112
|
adantr |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
114 |
94 113
|
reximddv2 |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) |
115 |
23 28 114
|
3jca |
⊢ ( ( 𝜑 ∧ 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
116 |
|
df-3an |
⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ↔ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
117 |
4
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐺 ∈ TarskiG ) |
118 |
8
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ 𝑃 ) |
119 |
9
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ∈ 𝑃 ) |
120 |
10
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ∈ 𝑃 ) |
121 |
5
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ∈ 𝑃 ) |
122 |
6
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ∈ 𝑃 ) |
123 |
7
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ 𝑃 ) |
124 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑦 ∈ 𝑃 ) |
125 |
|
simp-5r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑥 ∈ 𝑃 ) |
126 |
|
simpllr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑧 ∈ 𝑃 ) |
127 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑡 ∈ 𝑃 ) |
128 |
|
eqid |
⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 ) |
129 |
|
simpr1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ) |
130 |
129
|
simplld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ) |
131 |
|
simpr2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ) |
132 |
131
|
simplld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ) |
133 |
1 3 2 117 119 118 126 132
|
tgbtwncom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ ( 𝑧 𝐼 𝐸 ) ) |
134 |
131
|
simplrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) |
135 |
134
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝑧 ) ) |
136 |
1 3 2 117 122 121 118 126 135
|
tgcgrcomr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝑧 − 𝐷 ) ) |
137 |
129
|
simplrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) |
138 |
1 3 2 117 121 125 119 118 137
|
tgcgrcomr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐷 − 𝐸 ) ) |
139 |
1 3 2 117 122 121 125 126 118 119 130 133 136 138
|
tgcgrextend |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝑥 ) = ( 𝑧 − 𝐸 ) ) |
140 |
1 3 2 117 122 125 126 119 139
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑥 − 𝐵 ) = ( 𝑧 − 𝐸 ) ) |
141 |
129
|
simprld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ) |
142 |
1 3 2 117 122 123 124 141
|
tgbtwncom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ ( 𝑦 𝐼 𝐵 ) ) |
143 |
131
|
simprld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ) |
144 |
129
|
simprrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) |
145 |
1 3 2 117 123 124 119 120 144
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝐶 ) = ( 𝐸 − 𝐹 ) ) |
146 |
131
|
simprrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) |
147 |
146
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝑡 ) ) |
148 |
1 3 2 117 122 123 120 127 147
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝑡 ) ) |
149 |
1 3 2 117 124 123 122 119 120 127 142 143 145 148
|
tgcgrextend |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝐵 ) = ( 𝐸 − 𝑡 ) ) |
150 |
1 3 2 117 124 122 119 127 149
|
tgcgrcoml |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝑦 ) = ( 𝐸 − 𝑡 ) ) |
151 |
|
simpr3 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) |
152 |
1 3 2 117 125 124 126 127 151
|
tgcgrcomlr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝑥 ) = ( 𝑡 − 𝑧 ) ) |
153 |
1 3 128 117 125 122 124 126 119 127 140 150 152
|
trgcgr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝑥 𝐵 𝑦 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑧 𝐸 𝑡 ”〉 ) |
154 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) |
155 |
154
|
simprld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ≠ 𝐸 ) |
156 |
1 3 2 117 119 118 126 132 155
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ≠ 𝑧 ) |
157 |
1 2 11 119 126 118 117 122 132 156 155
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑧 ) |
158 |
1 2 11 118 126 119 117 157
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ) |
159 |
154
|
simprrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ≠ 𝐸 ) |
160 |
1 3 2 117 119 120 127 143 159
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ≠ 𝑡 ) |
161 |
1 2 11 119 127 120 117 122 143 160 159
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑡 ) |
162 |
1 2 11 120 127 119 117 161
|
hlcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) |
163 |
1 2 11 117 125 122 124 118 119 120 126 127 153 158 162
|
iscgrad |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝑥 𝐵 𝑦 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
164 |
1 2 117 11 125 122 124 118 119 120 163
|
cgracom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑥 𝐵 𝑦 ”〉 ) |
165 |
154
|
simplld |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ≠ 𝐵 ) |
166 |
1 3 2 117 122 121 125 130 165
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ≠ 𝑥 ) |
167 |
1 2 11 122 125 121 117 121 130 166 165
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑥 ) |
168 |
1 2 11 117 118 119 120 125 122 124 164 121 167
|
cgrahl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐴 𝐵 𝑦 ”〉 ) |
169 |
154
|
simplrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ≠ 𝐵 ) |
170 |
1 3 2 117 122 123 124 141 169
|
tgbtwnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ≠ 𝑦 ) |
171 |
1 2 11 122 124 123 117 121 141 170 169
|
btwnhl1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑦 ) |
172 |
1 2 11 117 118 119 120 121 122 124 168 123 171
|
cgrahl2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝐷 𝐸 𝐹 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐴 𝐵 𝐶 ”〉 ) |
173 |
1 2 117 11 118 119 120 121 122 123 172
|
cgracom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
174 |
173
|
adantl3r |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
175 |
|
simpr |
⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) |
176 |
|
oveq2 |
⊢ ( 𝑑 = 𝑧 → ( 𝐸 𝐼 𝑑 ) = ( 𝐸 𝐼 𝑧 ) ) |
177 |
176
|
eleq2d |
⊢ ( 𝑑 = 𝑧 → ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ↔ 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ) ) |
178 |
|
oveq2 |
⊢ ( 𝑑 = 𝑧 → ( 𝐷 − 𝑑 ) = ( 𝐷 − 𝑧 ) ) |
179 |
178
|
eqeq1d |
⊢ ( 𝑑 = 𝑧 → ( ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ↔ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ) |
180 |
177 179
|
anbi12d |
⊢ ( 𝑑 = 𝑧 → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ↔ ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ) ) |
181 |
180
|
anbi1d |
⊢ ( 𝑑 = 𝑧 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
182 |
|
oveq1 |
⊢ ( 𝑑 = 𝑧 → ( 𝑑 − 𝑓 ) = ( 𝑧 − 𝑓 ) ) |
183 |
182
|
eqeq2d |
⊢ ( 𝑑 = 𝑧 → ( ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) ) |
184 |
181 183
|
3anbi23d |
⊢ ( 𝑑 = 𝑧 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) ) ) |
185 |
|
oveq2 |
⊢ ( 𝑓 = 𝑡 → ( 𝐸 𝐼 𝑓 ) = ( 𝐸 𝐼 𝑡 ) ) |
186 |
185
|
eleq2d |
⊢ ( 𝑓 = 𝑡 → ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ↔ 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ) ) |
187 |
|
oveq2 |
⊢ ( 𝑓 = 𝑡 → ( 𝐹 − 𝑓 ) = ( 𝐹 − 𝑡 ) ) |
188 |
187
|
eqeq1d |
⊢ ( 𝑓 = 𝑡 → ( ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ↔ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) |
189 |
186 188
|
anbi12d |
⊢ ( 𝑓 = 𝑡 → ( ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ↔ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ) |
190 |
189
|
anbi2d |
⊢ ( 𝑓 = 𝑡 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ) ) |
191 |
|
oveq2 |
⊢ ( 𝑓 = 𝑡 → ( 𝑧 − 𝑓 ) = ( 𝑧 − 𝑡 ) ) |
192 |
191
|
eqeq2d |
⊢ ( 𝑓 = 𝑡 → ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) |
193 |
190 192
|
3anbi23d |
⊢ ( 𝑓 = 𝑡 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) ) |
194 |
184 193
|
cbvrex2vw |
⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) |
195 |
175 194
|
sylib |
⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) |
196 |
174 195
|
r19.29vva |
⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
197 |
196
|
adantl3r |
⊢ ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
198 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) |
199 |
|
oveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝐵 𝐼 𝑎 ) = ( 𝐵 𝐼 𝑥 ) ) |
200 |
199
|
eleq2d |
⊢ ( 𝑎 = 𝑥 → ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ↔ 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ) ) |
201 |
|
oveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝐴 − 𝑎 ) = ( 𝐴 − 𝑥 ) ) |
202 |
201
|
eqeq1d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ↔ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ) |
203 |
200 202
|
anbi12d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ↔ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ) ) |
204 |
203
|
anbi1d |
⊢ ( 𝑎 = 𝑥 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ) |
205 |
|
oveq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 − 𝑐 ) = ( 𝑥 − 𝑐 ) ) |
206 |
205
|
eqeq1d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) |
207 |
204 206
|
3anbi13d |
⊢ ( 𝑎 = 𝑥 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
208 |
207
|
2rexbidv |
⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) |
209 |
|
oveq2 |
⊢ ( 𝑐 = 𝑦 → ( 𝐵 𝐼 𝑐 ) = ( 𝐵 𝐼 𝑦 ) ) |
210 |
209
|
eleq2d |
⊢ ( 𝑐 = 𝑦 → ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ↔ 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ) ) |
211 |
|
oveq2 |
⊢ ( 𝑐 = 𝑦 → ( 𝐶 − 𝑐 ) = ( 𝐶 − 𝑦 ) ) |
212 |
211
|
eqeq1d |
⊢ ( 𝑐 = 𝑦 → ( ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ↔ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) |
213 |
210 212
|
anbi12d |
⊢ ( 𝑐 = 𝑦 → ( ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ↔ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ) |
214 |
213
|
anbi2d |
⊢ ( 𝑐 = 𝑦 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ) ) |
215 |
|
oveq2 |
⊢ ( 𝑐 = 𝑦 → ( 𝑥 − 𝑐 ) = ( 𝑥 − 𝑦 ) ) |
216 |
215
|
eqeq1d |
⊢ ( 𝑐 = 𝑦 → ( ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) |
217 |
214 216
|
3anbi13d |
⊢ ( 𝑐 = 𝑦 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) ) |
218 |
217
|
2rexbidv |
⊢ ( 𝑐 = 𝑦 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) ) |
219 |
208 218
|
cbvrex2vw |
⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) |
220 |
198 219
|
sylib |
⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) |
221 |
197 220
|
r19.29vva |
⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
222 |
221
|
anasss |
⊢ ( ( 𝜑 ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
223 |
116 222
|
sylan2b |
⊢ ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
224 |
115 223
|
impbida |
⊢ ( 𝜑 → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) ) |