Step |
Hyp |
Ref |
Expression |
1 |
|
hpg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
hpg.d |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
hpg.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
hpg.o |
⊢ 𝑂 = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } |
5 |
|
opphl.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
6 |
|
opphl.d |
⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 ) |
7 |
|
opphl.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
8 |
|
opphl.k |
⊢ 𝐾 = ( hlG ‘ 𝐺 ) |
9 |
|
opphllem5.n |
⊢ 𝑁 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) |
10 |
|
opphllem5.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
11 |
|
opphllem5.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑃 ) |
12 |
|
opphllem5.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝐷 ) |
13 |
|
opphllem5.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝐷 ) |
14 |
|
opphllem5.m |
⊢ ( 𝜑 → 𝑀 ∈ 𝑃 ) |
15 |
|
opphllem5.o |
⊢ ( 𝜑 → 𝐴 𝑂 𝐶 ) |
16 |
|
opphllem5.p |
⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) ) |
17 |
|
opphllem5.q |
⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) ) |
18 |
|
opphllem3.t |
⊢ ( 𝜑 → 𝑅 ≠ 𝑆 ) |
19 |
|
opphllem3.l |
⊢ ( 𝜑 → ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ) |
20 |
|
opphllem3.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑃 ) |
21 |
|
opphllem3.v |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝑅 ) = 𝑆 ) |
22 |
20
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑈 ∈ 𝑃 ) |
23 |
10
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐴 ∈ 𝑃 ) |
24 |
1 5 3 7 6 12
|
tglnpt |
⊢ ( 𝜑 → 𝑅 ∈ 𝑃 ) |
25 |
24
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑅 ∈ 𝑃 ) |
26 |
7
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐺 ∈ TarskiG ) |
27 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑝 ∈ 𝑃 ) |
28 |
|
simprl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ) |
29 |
5 7 16
|
perpln2 |
⊢ ( 𝜑 → ( 𝐴 𝐿 𝑅 ) ∈ ran 𝐿 ) |
30 |
1 3 5 7 10 24 29
|
tglnne |
⊢ ( 𝜑 → 𝐴 ≠ 𝑅 ) |
31 |
30
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐴 ≠ 𝑅 ) |
32 |
11
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐶 ∈ 𝑃 ) |
33 |
1 5 3 7 6 13
|
tglnpt |
⊢ ( 𝜑 → 𝑆 ∈ 𝑃 ) |
34 |
33
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑆 ∈ 𝑃 ) |
35 |
|
simprr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) |
36 |
1 2 3 26 34 32 25 27 35
|
tgcgrcomlr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝐶 − 𝑆 ) = ( 𝑝 − 𝑅 ) ) |
37 |
17
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑆 ) ) |
38 |
5 26 37
|
perpln2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝐶 𝐿 𝑆 ) ∈ ran 𝐿 ) |
39 |
1 3 5 26 32 34 38
|
tglnne |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐶 ≠ 𝑆 ) |
40 |
1 2 3 26 32 34 27 25 36 39
|
tgcgrneq |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑝 ≠ 𝑅 ) |
41 |
1 3 8 22 23 25 26 27 28 31 40
|
hlbtwn |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) ) |
42 |
|
eqid |
⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 ) |
43 |
26
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝐺 ∈ TarskiG ) |
44 |
14
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝑀 ∈ 𝑃 ) |
45 |
22
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝑈 ∈ 𝑃 ) |
46 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝑝 ∈ 𝑃 ) |
47 |
25
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝑅 ∈ 𝑃 ) |
48 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) |
49 |
1 2 3 5 42 43 9 8 44 45 46 47 48
|
mirhl |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ ( 𝑁 ‘ 𝑅 ) ) ( 𝑁 ‘ 𝑝 ) ) |
50 |
|
eqidd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝑁 ‘ 𝑈 ) = ( 𝑁 ‘ 𝑈 ) ) |
51 |
21
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝑁 ‘ 𝑅 ) = 𝑆 ) |
52 |
51
|
fveq2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝐾 ‘ ( 𝑁 ‘ 𝑅 ) ) = ( 𝐾 ‘ 𝑆 ) ) |
53 |
|
simprr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) |
54 |
26
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝐺 ∈ TarskiG ) |
55 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑚 ∈ 𝑃 ) |
56 |
14
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑀 ∈ 𝑃 ) |
57 |
34
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑆 ∈ 𝑃 ) |
58 |
25
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑅 ∈ 𝑃 ) |
59 |
|
simprl |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ) |
60 |
59
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) = 𝑅 ) |
61 |
9
|
fveq1i |
⊢ ( 𝑁 ‘ 𝑆 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 ) |
62 |
1 2 3 5 42 7 14 9 24 21
|
mircom |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = 𝑅 ) |
63 |
61 62
|
eqtr3id |
⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 ) = 𝑅 ) |
64 |
63
|
ad6antr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ‘ 𝑆 ) = 𝑅 ) |
65 |
1 2 3 5 42 54 55 56 57 58 60 64
|
miduniq |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → 𝑚 = 𝑀 ) |
66 |
65
|
fveq2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 ) ) |
67 |
66 9
|
eqtr4di |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = 𝑁 ) |
68 |
67
|
fveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) = ( 𝑁 ‘ 𝑝 ) ) |
69 |
53 68
|
eqtr2d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑚 ∈ 𝑃 ) ∧ ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) → ( 𝑁 ‘ 𝑝 ) = 𝐶 ) |
70 |
18
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑅 ≠ 𝑆 ) |
71 |
70
|
necomd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑆 ≠ 𝑅 ) |
72 |
6
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐷 ∈ ran 𝐿 ) |
73 |
|
simp-4r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑡 ∈ 𝐷 ) |
74 |
1 5 3 26 72 73
|
tglnpt |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑡 ∈ 𝑃 ) |
75 |
13
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑆 ∈ 𝐷 ) |
76 |
12
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑅 ∈ 𝐷 ) |
77 |
1 3 5 26 34 25 71 71 72 75 76
|
tglinethru |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐷 = ( 𝑆 𝐿 𝑅 ) ) |
78 |
16
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) ) |
79 |
77 78
|
eqbrtrrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑆 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑅 ) ) |
80 |
1 3 5 26 32 34 39
|
tglinecom |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝐶 𝐿 𝑆 ) = ( 𝑆 𝐿 𝐶 ) ) |
81 |
37 77 80
|
3brtr3d |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑆 𝐿 𝑅 ) ( ⟂G ‘ 𝐺 ) ( 𝑆 𝐿 𝐶 ) ) |
82 |
73 77
|
eleqtrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑡 ∈ ( 𝑆 𝐿 𝑅 ) ) |
83 |
|
simpllr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) |
84 |
1 2 3 5 26 42 34 25 71 23 32 74 79 81 82 83 27 28 35
|
opphllem |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ∃ 𝑚 ∈ 𝑃 ( 𝑅 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑆 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑝 ) ) ) |
85 |
69 84
|
r19.29a |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑁 ‘ 𝑝 ) = 𝐶 ) |
86 |
85
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝑁 ‘ 𝑝 ) = 𝐶 ) |
87 |
50 52 86
|
breq123d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ ( 𝑁 ‘ 𝑅 ) ) ( 𝑁 ‘ 𝑝 ) ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) ) |
88 |
49 87
|
mpbid |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) → ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) |
89 |
26
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝐺 ∈ TarskiG ) |
90 |
14
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑀 ∈ 𝑃 ) |
91 |
1 2 3 5 42 7 14 9 20
|
mircl |
⊢ ( 𝜑 → ( 𝑁 ‘ 𝑈 ) ∈ 𝑃 ) |
92 |
91
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝑈 ) ∈ 𝑃 ) |
93 |
32
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝐶 ∈ 𝑃 ) |
94 |
34
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑆 ∈ 𝑃 ) |
95 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) |
96 |
1 2 3 5 42 89 9 8 90 92 93 94 95
|
mirhl |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) ( 𝐾 ‘ ( 𝑁 ‘ 𝑆 ) ) ( 𝑁 ‘ 𝐶 ) ) |
97 |
22
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑈 ∈ 𝑃 ) |
98 |
1 2 3 5 42 89 90 9 97
|
mirmir |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) = 𝑈 ) |
99 |
25
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑅 ∈ 𝑃 ) |
100 |
21
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝑅 ) = 𝑆 ) |
101 |
1 2 3 5 42 89 90 9 99 100
|
mircom |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝑆 ) = 𝑅 ) |
102 |
101
|
fveq2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝐾 ‘ ( 𝑁 ‘ 𝑆 ) ) = ( 𝐾 ‘ 𝑅 ) ) |
103 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑝 ∈ 𝑃 ) |
104 |
85
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝑝 ) = 𝐶 ) |
105 |
1 2 3 5 42 89 90 9 103 104
|
mircom |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( 𝑁 ‘ 𝐶 ) = 𝑝 ) |
106 |
98 102 105
|
breq123d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑈 ) ) ( 𝐾 ‘ ( 𝑁 ‘ 𝑆 ) ) ( 𝑁 ‘ 𝐶 ) ↔ 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) ) |
107 |
96 106
|
mpbid |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ∧ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) → 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ) |
108 |
88 107
|
impbida |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝑝 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) ) |
109 |
41 108
|
bitrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) ) |
110 |
|
eqid |
⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 ) |
111 |
1 2 3 110 7 33 11 24 10
|
legov |
⊢ ( 𝜑 → ( ( 𝑆 − 𝐶 ) ( ≤G ‘ 𝐺 ) ( 𝑅 − 𝐴 ) ↔ ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) ) |
112 |
19 111
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) |
113 |
112
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ( 𝑅 𝐼 𝐴 ) ∧ ( 𝑆 − 𝐶 ) = ( 𝑅 − 𝑝 ) ) ) |
114 |
109 113
|
r19.29a |
⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) ) |
115 |
1 2 3 4 10 11
|
islnopp |
⊢ ( 𝜑 → ( 𝐴 𝑂 𝐶 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ) ) |
116 |
15 115
|
mpbid |
⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) ) |
117 |
116
|
simprd |
⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐶 ) ) |
118 |
114 117
|
r19.29a |
⊢ ( 𝜑 → ( 𝑈 ( 𝐾 ‘ 𝑅 ) 𝐴 ↔ ( 𝑁 ‘ 𝑈 ) ( 𝐾 ‘ 𝑆 ) 𝐶 ) ) |