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 |
|
sacgr.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) |
12 |
|
sacgr.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) |
13 |
|
sacgr.1 |
⊢ ( 𝜑 → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
14 |
|
sacgr.2 |
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝑋 ) ) |
15 |
|
sacgr.3 |
⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝑌 ) ) |
16 |
|
sacgr.4 |
⊢ ( 𝜑 → 𝐵 ≠ 𝑋 ) |
17 |
|
sacgr.5 |
⊢ ( 𝜑 → 𝐸 ≠ 𝑌 ) |
18 |
|
eqid |
⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 ) |
19 |
4
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG ) |
20 |
11
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑋 ∈ 𝑃 ) |
21 |
6
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ∈ 𝑃 ) |
22 |
7
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 ) |
23 |
12
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌 ∈ 𝑃 ) |
24 |
9
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 ) |
25 |
10
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 ) |
26 |
|
eqid |
⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 ) |
27 |
|
eqid |
⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 ) |
28 |
|
eqid |
⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) |
29 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 ) |
30 |
1 3 2 26 27 19 24 28 29
|
mircl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ∈ 𝑃 ) |
31 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 ) |
32 |
|
eqid |
⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) |
33 |
1 3 2 26 27 4 6 32 11
|
mirmir |
⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) = 𝑋 ) |
34 |
|
eqidd |
⊢ ( 𝜑 → 𝐵 = 𝐵 ) |
35 |
|
eqidd |
⊢ ( 𝜑 → 𝐶 = 𝐶 ) |
36 |
33 34 35
|
s3eqd |
⊢ ( 𝜑 → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”〉 = 〈“ 𝑋 𝐵 𝐶 ”〉 ) |
37 |
36
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”〉 = 〈“ 𝑋 𝐵 𝐶 ”〉 ) |
38 |
|
eqid |
⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 ) |
39 |
1 3 2 26 27 4 6 32 11
|
mircl |
⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ∈ 𝑃 ) |
40 |
39
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ∈ 𝑃 ) |
41 |
16
|
necomd |
⊢ ( 𝜑 → 𝑋 ≠ 𝐵 ) |
42 |
1 3 2 26 27 4 6 32 11 41
|
mirne |
⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ≠ 𝐵 ) |
43 |
42
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ≠ 𝐵 ) |
44 |
|
simpr1 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ) |
45 |
1 3 2 26 27 19 38 32 28 40 21 29 24 22 31 43 44
|
mirtrcgr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) 𝐸 𝑦 ”〉 ) |
46 |
37 45
|
eqbrtrrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 〈“ 𝑋 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) 𝐸 𝑦 ”〉 ) |
47 |
17
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ≠ 𝑌 ) |
48 |
47
|
necomd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌 ≠ 𝐸 ) |
49 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 ) |
50 |
|
simpr2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ) |
51 |
1 2 18 29 49 24 19 50
|
hlne1 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ≠ 𝐸 ) |
52 |
1 3 2 26 27 19 24 28 29 51
|
mirne |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ≠ 𝐸 ) |
53 |
1 2 18 29 49 24 19 50
|
hlcomd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑥 ) |
54 |
15
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑌 ) ) |
55 |
1 2 18 49 29 23 19 24 53 54
|
btwnhl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑥 𝐼 𝑌 ) ) |
56 |
1 3 2 19 29 24 23 55
|
tgbtwncom |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑌 𝐼 𝑥 ) ) |
57 |
1 3 2 26 27 19 24 28 29
|
mirmir |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) = 𝑥 ) |
58 |
57
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( 𝑌 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) ) = ( 𝑌 𝐼 𝑥 ) ) |
59 |
56 58
|
eleqtrrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ ( 𝑌 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) ) ) |
60 |
1 3 2 26 27 19 28 18 24 23 30 24 48 52 59
|
mirhl2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑌 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ) |
61 |
1 2 18 23 30 24 19 60
|
hlcomd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐸 ) ‘ 𝑥 ) ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑌 ) |
62 |
|
simpr3 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) |
63 |
1 2 18 19 20 21 22 23 24 25 30 31 46 61 62
|
iscgrad |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) → 〈“ 𝑋 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑌 𝐸 𝐹 ”〉 ) |
64 |
1 2 18 4 5 6 7 8 9 10 13
|
cgrane2 |
⊢ ( 𝜑 → 𝐵 ≠ 𝐶 ) |
65 |
1 2 4 18 39 6 7 42 64
|
cgraid |
⊢ ( 𝜑 → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ) |
66 |
1 2 18 4 5 6 7 8 9 10 13
|
cgrane1 |
⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) |
67 |
33
|
oveq2d |
⊢ ( 𝜑 → ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) ) = ( 𝐴 𝐼 𝑋 ) ) |
68 |
14 67
|
eleqtrrd |
⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) ) ) |
69 |
1 3 2 26 27 4 32 18 6 5 39 5 66 42 68
|
mirhl2 |
⊢ ( 𝜑 → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) ) |
70 |
1 2 18 4 39 6 7 39 6 7 65 5 69
|
cgrahl1 |
⊢ ( 𝜑 → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐴 𝐵 𝐶 ”〉 ) |
71 |
1 2 4 18 39 6 7 5 6 7 70 8 9 10 13
|
cgratr |
⊢ ( 𝜑 → 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ) |
72 |
1 2 18 4 39 6 7 8 9 10
|
iscgra |
⊢ ( 𝜑 → ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝐹 ”〉 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) ) |
73 |
71 72
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 〈“ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝑋 ) 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝑥 𝐸 𝑦 ”〉 ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) |
74 |
63 73
|
r19.29vva |
⊢ ( 𝜑 → 〈“ 𝑋 𝐵 𝐶 ”〉 ( cgrA ‘ 𝐺 ) 〈“ 𝑌 𝐸 𝐹 ”〉 ) |