Step |
Hyp |
Ref |
Expression |
1 |
|
trgcopy.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
trgcopy.m |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
trgcopy.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
trgcopy.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
5 |
|
trgcopy.k |
⊢ 𝐾 = ( hlG ‘ 𝐺 ) |
6 |
|
trgcopy.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
7 |
|
trgcopy.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
8 |
|
trgcopy.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) |
9 |
|
trgcopy.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) |
10 |
|
trgcopy.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑃 ) |
11 |
|
trgcopy.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) |
12 |
|
trgcopy.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝑃 ) |
13 |
|
trgcopy.1 |
⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) |
14 |
|
trgcopy.2 |
⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) ) |
15 |
|
trgcopy.3 |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) |
16 |
|
eqid |
⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 ) |
17 |
6
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG ) |
18 |
17
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐺 ∈ TarskiG ) |
19 |
18
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝐺 ∈ TarskiG ) |
20 |
19
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG ) |
21 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 ) |
22 |
21
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐴 ∈ 𝑃 ) |
23 |
22
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 ) |
24 |
8
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐵 ∈ 𝑃 ) |
26 |
25
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 ) |
27 |
9
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝐶 ∈ 𝑃 ) |
28 |
27
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 ) |
29 |
10
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐷 ∈ 𝑃 ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐷 ∈ 𝑃 ) |
31 |
30
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐷 ∈ 𝑃 ) |
32 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐸 ∈ 𝑃 ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐸 ∈ 𝑃 ) |
34 |
33
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐸 ∈ 𝑃 ) |
35 |
|
simprl |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ∈ 𝑃 ) |
36 |
15
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) |
37 |
36
|
ad5antr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) ) |
38 |
1 4 3 6 8 9 7 13
|
ncoltgdim2 |
⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 ) |
39 |
38
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐺 DimTarskiG≥ 2 ) |
40 |
39
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐺 DimTarskiG≥ 2 ) |
41 |
1 3 4 6 7 8 9 13
|
ncolne1 |
⊢ ( 𝜑 → 𝐴 ≠ 𝐵 ) |
42 |
1 3 4 6 7 8 41
|
tgelrnln |
⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 ) |
43 |
42
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 ) |
44 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) |
45 |
1 4 3 17 43 44
|
tglnpt |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ∈ 𝑃 ) |
46 |
45
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝑥 ∈ 𝑃 ) |
47 |
46
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑥 ∈ 𝑃 ) |
48 |
47
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 ) |
49 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝑦 ∈ 𝑃 ) |
50 |
49
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑦 ∈ 𝑃 ) |
51 |
50
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 ) |
52 |
44
|
ad5antr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) |
53 |
41
|
ad7antr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐴 ≠ 𝐵 ) |
54 |
1 3 4 20 23 26 53
|
tglinecom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) ) |
55 |
52 54
|
eleqtrd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑥 ∈ ( 𝐵 𝐿 𝐴 ) ) |
56 |
|
simp-6r |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) |
57 |
4 20 56
|
perpln1 |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐶 𝐿 𝑥 ) ∈ ran 𝐿 ) |
58 |
43
|
ad5antr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 ) |
59 |
1 2 3 4 20 57 58 56
|
perpcom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑥 ) ) |
60 |
1 4 3 6 8 9 7 13
|
ncolrot2 |
⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) |
61 |
|
ioran |
⊢ ( ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ↔ ( ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) ) |
62 |
60 61
|
sylib |
⊢ ( 𝜑 → ( ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) ) |
63 |
62
|
simpld |
⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) |
64 |
63
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) |
65 |
|
nelne2 |
⊢ ( ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ≠ 𝐶 ) |
66 |
44 64 65
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ≠ 𝐶 ) |
67 |
66
|
ad4antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑥 ≠ 𝐶 ) |
68 |
67
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑥 ≠ 𝐶 ) |
69 |
68
|
necomd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐶 ≠ 𝑥 ) |
70 |
1 3 4 20 28 48 69
|
tglinecom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐶 𝐿 𝑥 ) = ( 𝑥 𝐿 𝐶 ) ) |
71 |
59 54 70
|
3brtr3d |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐵 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝑥 𝐿 𝐶 ) ) |
72 |
1 2 3 4 20 26 23 55 28 71
|
perprag |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐵 𝑥 𝐶 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
73 |
1 3 4 6 10 11 12 14
|
ncolne1 |
⊢ ( 𝜑 → 𝐷 ≠ 𝐸 ) |
74 |
73
|
necomd |
⊢ ( 𝜑 → 𝐸 ≠ 𝐷 ) |
75 |
74
|
ad7antr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐸 ≠ 𝐷 ) |
76 |
73
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐷 ≠ 𝐸 ) |
77 |
76
|
neneqd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ¬ 𝐷 = 𝐸 ) |
78 |
44
|
orcd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) |
79 |
1 4 3 17 21 24 45 78
|
colrot2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐵 ∈ ( 𝑥 𝐿 𝐴 ) ∨ 𝑥 = 𝐴 ) ) |
80 |
1 4 3 17 45 21 24 79
|
colcom |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ) |
81 |
80
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝑥 ) ∨ 𝐴 = 𝑥 ) ) |
82 |
|
simpr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) |
83 |
1 4 3 18 22 25 46 16 30 33 49 81 82
|
lnxfr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝐸 ∈ ( 𝐷 𝐿 𝑦 ) ∨ 𝐷 = 𝑦 ) ) |
84 |
1 4 3 18 30 49 33 83
|
colrot2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝑦 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) ) |
85 |
1 4 3 18 33 30 49 84
|
colcom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) |
86 |
85
|
orcomd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝐷 = 𝐸 ∨ 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ) ) |
87 |
86
|
ord |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( ¬ 𝐷 = 𝐸 → 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ) ) |
88 |
77 87
|
mpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ) |
89 |
88
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ) |
90 |
1 3 4 20 34 31 51 75 89
|
lncom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑦 ∈ ( 𝐸 𝐿 𝐷 ) ) |
91 |
|
simprrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) |
92 |
91
|
eqcomd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑥 − 𝐶 ) = ( 𝑦 − 𝑓 ) ) |
93 |
1 2 3 20 48 28 51 35 92 68
|
tgcgrneq |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑦 ≠ 𝑓 ) |
94 |
1 3 4 20 51 35 93
|
tgelrnln |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 𝐿 𝑓 ) ∈ ran 𝐿 ) |
95 |
1 3 4 20 34 31 75
|
tgelrnln |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐸 𝐿 𝐷 ) ∈ ran 𝐿 ) |
96 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑞 ∈ 𝑃 ) |
97 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑞 ∈ 𝑃 ) |
98 |
|
simprl |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ) |
99 |
4 19 98
|
perpln2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → ( 𝑞 𝐿 𝑦 ) ∈ ran 𝐿 ) |
100 |
1 3 4 19 97 50 99
|
tglnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑞 ≠ 𝑦 ) |
101 |
100
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑞 ≠ 𝑦 ) |
102 |
101
|
necomd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑦 ≠ 𝑞 ) |
103 |
1 3 4 20 51 96 102
|
tgelrnln |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 𝐿 𝑞 ) ∈ ran 𝐿 ) |
104 |
98
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ) |
105 |
1 3 4 20 34 31 75
|
tglinecom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐸 𝐿 𝐷 ) = ( 𝐷 𝐿 𝐸 ) ) |
106 |
1 3 4 20 51 96 102
|
tglinecom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 𝐿 𝑞 ) = ( 𝑞 𝐿 𝑦 ) ) |
107 |
104 105 106
|
3brtr4d |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐸 𝐿 𝐷 ) ( ⟂G ‘ 𝐺 ) ( 𝑦 𝐿 𝑞 ) ) |
108 |
1 2 3 4 20 95 103 107
|
perpcom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐸 𝐿 𝐷 ) ) |
109 |
|
simprrl |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ) |
110 |
1 3 5 35 96 51 20 4 109
|
hlln |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ∈ ( 𝑞 𝐿 𝑦 ) ) |
111 |
1 3 4 20 51 96 35 102 110
|
lncom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ∈ ( 𝑦 𝐿 𝑞 ) ) |
112 |
111
|
orcd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑓 ∈ ( 𝑦 𝐿 𝑞 ) ∨ 𝑦 = 𝑞 ) ) |
113 |
1 2 3 4 20 51 96 35 108 112 93
|
colperp |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑦 𝐿 𝑓 ) ( ⟂G ‘ 𝐺 ) ( 𝐸 𝐿 𝐷 ) ) |
114 |
1 2 3 4 20 94 95 113
|
perpcom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐸 𝐿 𝐷 ) ( ⟂G ‘ 𝐺 ) ( 𝑦 𝐿 𝑓 ) ) |
115 |
1 2 3 4 20 34 31 90 35 114
|
perprag |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐸 𝑦 𝑓 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
116 |
82
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) |
117 |
1 2 3 16 20 23 26 48 31 34 51 116
|
cgr3simp2 |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐵 − 𝑥 ) = ( 𝐸 − 𝑦 ) ) |
118 |
1 2 3 20 40 26 48 28 34 51 35 72 115 117 92
|
hypcgr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑓 ) ) |
119 |
|
eqid |
⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 ) |
120 |
54 71
|
eqbrtrd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑥 𝐿 𝐶 ) ) |
121 |
1 2 3 4 20 23 26 52 28 120
|
perprag |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐴 𝑥 𝐶 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
122 |
1 2 3 4 119 20 23 48 28 121
|
ragcom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐶 𝑥 𝐴 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
123 |
105 114
|
eqbrtrrd |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑦 𝐿 𝑓 ) ) |
124 |
1 2 3 4 20 31 34 89 35 123
|
perprag |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐷 𝑦 𝑓 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
125 |
1 2 3 4 119 20 31 51 35 124
|
ragcom |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝑓 𝑦 𝐷 ”〉 ∈ ( ∟G ‘ 𝐺 ) ) |
126 |
1 2 3 20 48 28 51 35 92
|
tgcgrcomlr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐶 − 𝑥 ) = ( 𝑓 − 𝑦 ) ) |
127 |
1 2 3 16 20 23 26 48 31 34 51 116
|
cgr3simp3 |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝑥 − 𝐴 ) = ( 𝑦 − 𝐷 ) ) |
128 |
1 2 3 20 40 28 48 23 35 51 31 122 125 126 127
|
hypcgr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝑓 − 𝐷 ) ) |
129 |
1 2 16 20 23 26 28 31 34 35 37 118 128
|
trgcgr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ) |
130 |
1 3 4 6 10 11 73
|
tgelrnln |
⊢ ( 𝜑 → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 ) |
131 |
130
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 ) |
132 |
131
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 ) |
133 |
|
simpl |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → 𝑤 = 𝑘 ) |
134 |
133
|
eleq1d |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → ( 𝑤 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ↔ 𝑘 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ) |
135 |
|
simpr |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → 𝑣 = 𝑙 ) |
136 |
135
|
eleq1d |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → ( 𝑣 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ↔ 𝑙 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ) |
137 |
134 136
|
anbi12d |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → ( ( 𝑤 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ↔ ( 𝑘 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑙 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ) ) |
138 |
|
simpr |
⊢ ( ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) ∧ 𝑧 = 𝑗 ) → 𝑧 = 𝑗 ) |
139 |
|
simpll |
⊢ ( ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) ∧ 𝑧 = 𝑗 ) → 𝑤 = 𝑘 ) |
140 |
|
simplr |
⊢ ( ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) ∧ 𝑧 = 𝑗 ) → 𝑣 = 𝑙 ) |
141 |
139 140
|
oveq12d |
⊢ ( ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) ∧ 𝑧 = 𝑗 ) → ( 𝑤 𝐼 𝑣 ) = ( 𝑘 𝐼 𝑙 ) ) |
142 |
138 141
|
eleq12d |
⊢ ( ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) ∧ 𝑧 = 𝑗 ) → ( 𝑧 ∈ ( 𝑤 𝐼 𝑣 ) ↔ 𝑗 ∈ ( 𝑘 𝐼 𝑙 ) ) ) |
143 |
142
|
cbvrexdva |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → ( ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑤 𝐼 𝑣 ) ↔ ∃ 𝑗 ∈ ( 𝐷 𝐿 𝐸 ) 𝑗 ∈ ( 𝑘 𝐼 𝑙 ) ) ) |
144 |
137 143
|
anbi12d |
⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑙 ) → ( ( ( 𝑤 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑤 𝐼 𝑣 ) ) ↔ ( ( 𝑘 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑙 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑗 ∈ ( 𝐷 𝐿 𝐸 ) 𝑗 ∈ ( 𝑘 𝐼 𝑙 ) ) ) ) |
145 |
144
|
cbvopabv |
⊢ { 〈 𝑤 , 𝑣 〉 ∣ ( ( 𝑤 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑤 𝐼 𝑣 ) ) } = { 〈 𝑘 , 𝑙 〉 ∣ ( ( 𝑘 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑙 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑗 ∈ ( 𝐷 𝐿 𝐸 ) 𝑗 ∈ ( 𝑘 𝐼 𝑙 ) ) } |
146 |
20
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐺 ∈ TarskiG ) |
147 |
28
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐶 ∈ 𝑃 ) |
148 |
26
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐵 ∈ 𝑃 ) |
149 |
23
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐴 ∈ 𝑃 ) |
150 |
31
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐷 ∈ 𝑃 ) |
151 |
34
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐸 ∈ 𝑃 ) |
152 |
35
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑓 ∈ 𝑃 ) |
153 |
74
|
ad8antr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐸 ≠ 𝐷 ) |
154 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) |
155 |
1 3 4 146 151 150 152 153 154
|
lncom |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑓 ∈ ( 𝐸 𝐿 𝐷 ) ) |
156 |
155
|
orcd |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝑓 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) ) |
157 |
1 4 3 146 151 150 152 156
|
colrot1 |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐸 ∈ ( 𝐷 𝐿 𝑓 ) ∨ 𝐷 = 𝑓 ) ) |
158 |
129
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ) |
159 |
1 2 3 16 146 149 148 147 150 151 152 158
|
trgcgrcom |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → 〈“ 𝐷 𝐸 𝑓 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐴 𝐵 𝐶 ”〉 ) |
160 |
1 4 3 146 150 151 152 16 149 148 147 157 159
|
lnxfr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) ) |
161 |
1 4 3 146 149 147 148 160
|
colrot1 |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) ) |
162 |
1 4 3 146 147 148 149 161
|
colcom |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) |
163 |
13
|
ad8antr |
⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) |
164 |
162 163
|
pm2.65da |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ¬ 𝑓 ∈ ( 𝐷 𝐿 𝐸 ) ) |
165 |
1 3 4 20 132 51 145 5 89 35 96 164 109
|
hphl |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝑞 ) |
166 |
12
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → 𝐹 ∈ 𝑃 ) |
167 |
166
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝐹 ∈ 𝑃 ) |
168 |
167
|
adantr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝐹 ∈ 𝑃 ) |
169 |
|
simplrr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) |
170 |
1 3 4 20 132 35 145 96 165 168 169
|
hpgtr |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) |
171 |
129 170
|
jca |
⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( 𝑓 ∈ 𝑃 ∧ ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) ) → ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |
172 |
1 3 5 50 47 27 19 97 2 100 67
|
hlcgrex |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → ∃ 𝑓 ∈ 𝑃 ( 𝑓 ( 𝐾 ‘ 𝑦 ) 𝑞 ∧ ( 𝑦 − 𝑓 ) = ( 𝑥 − 𝐶 ) ) ) |
173 |
171 172
|
reximddv |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → ∃ 𝑓 ∈ 𝑃 ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |
174 |
1 4 3 6 11 12 10 14
|
ncolrot2 |
⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) |
175 |
|
ioran |
⊢ ( ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ↔ ( ¬ 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ 𝐷 = 𝐸 ) ) |
176 |
174 175
|
sylib |
⊢ ( 𝜑 → ( ¬ 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ 𝐷 = 𝐸 ) ) |
177 |
176
|
simpld |
⊢ ( 𝜑 → ¬ 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ) |
178 |
177
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ¬ 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ) |
179 |
1 2 3 4 18 39 131 145 88 166 178
|
lnperpex |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ∃ 𝑞 ∈ 𝑃 ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝑦 ) ∧ 𝑞 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |
180 |
173 179
|
r19.29a |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) → ∃ 𝑓 ∈ 𝑃 ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |
181 |
1 4 3 17 21 24 45 16 29 32 2 80 36
|
lnext |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑦 ∈ 𝑃 〈“ 𝐴 𝐵 𝑥 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑦 ”〉 ) |
182 |
180 181
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑓 ∈ 𝑃 ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |
183 |
1 2 3 4 6 42 9 63
|
footex |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) |
184 |
182 183
|
r19.29a |
⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 〈“ 𝐴 𝐵 𝐶 ”〉 ( cgrG ‘ 𝐺 ) 〈“ 𝐷 𝐸 𝑓 ”〉 ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) |