| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ismid.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
| 2 |
|
ismid.d |
⊢ − = ( dist ‘ 𝐺 ) |
| 3 |
|
ismid.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
| 4 |
|
ismid.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
| 5 |
|
ismid.1 |
⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 ) |
| 6 |
|
lmieu.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
| 7 |
|
lmieu.1 |
⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 ) |
| 8 |
|
lmieu.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
| 9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 ) |
| 10 |
|
simpr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ¬ 𝐴 = 𝑏 ) |
| 11 |
|
eqidd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) |
| 12 |
4
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐺 ∈ TarskiG ) |
| 13 |
5
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐺 DimTarskiG≥ 2 ) |
| 14 |
9
|
ad3antrrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐴 ∈ 𝑃 ) |
| 15 |
|
simpllr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝑏 ∈ 𝑃 ) |
| 16 |
|
eqid |
⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 ) |
| 17 |
1 2 3 12 13 14 15
|
midcl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑃 ) |
| 18 |
1 2 3 12 13 14 15 16 17
|
ismidb |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ( 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ) |
| 19 |
11 18
|
mpbird |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ‘ 𝐴 ) ) |
| 20 |
19
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ‘ 𝐴 ) ) |
| 21 |
12
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐺 ∈ TarskiG ) |
| 22 |
7
|
ad4antr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐷 ∈ ran 𝐿 ) |
| 23 |
22
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐷 ∈ ran 𝐿 ) |
| 24 |
14
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 ∈ 𝑃 ) |
| 25 |
15
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝑏 ∈ 𝑃 ) |
| 26 |
10
|
neqned |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐴 ≠ 𝑏 ) |
| 27 |
26
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 ≠ 𝑏 ) |
| 28 |
1 3 6 21 24 25 27
|
tgelrnln |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( 𝐴 𝐿 𝑏 ) ∈ ran 𝐿 ) |
| 29 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) |
| 30 |
|
simp-4r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐴 ∈ 𝐷 ) |
| 31 |
30
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 ∈ 𝐷 ) |
| 32 |
1 3 6 21 24 25 27
|
tglinerflx1 |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 ∈ ( 𝐴 𝐿 𝑏 ) ) |
| 33 |
31 32
|
elind |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 ∈ ( 𝐷 ∩ ( 𝐴 𝐿 𝑏 ) ) ) |
| 34 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) |
| 35 |
1 2 3 12 13 14 15
|
midbtwn |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐴 𝐼 𝑏 ) ) |
| 36 |
1 3 6 12 14 15 17 26 35
|
btwnlng1 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐴 𝐿 𝑏 ) ) |
| 37 |
36
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐴 𝐿 𝑏 ) ) |
| 38 |
34 37
|
elind |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐷 ∩ ( 𝐴 𝐿 𝑏 ) ) ) |
| 39 |
1 3 6 21 23 28 29 33 38
|
tglineineq |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) |
| 40 |
39
|
fveq2d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ) |
| 41 |
40
|
fveq1d |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐴 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ‘ 𝐴 ) ) |
| 42 |
|
eqid |
⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) |
| 43 |
1 2 3 6 16 21 24 42
|
mircinv |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐴 ) = 𝐴 ) |
| 44 |
20 41 43
|
3eqtr2rd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) → 𝐴 = 𝑏 ) |
| 45 |
10 44
|
mtand |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ¬ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) |
| 46 |
4
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → 𝐺 ∈ TarskiG ) |
| 47 |
7
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → 𝐷 ∈ ran 𝐿 ) |
| 48 |
|
nne |
⊢ ( ¬ 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ↔ 𝐷 = ( 𝐴 𝐿 𝑏 ) ) |
| 49 |
45 48
|
sylib |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → 𝐷 = ( 𝐴 𝐿 𝑏 ) ) |
| 50 |
49
|
adantr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → 𝐷 = ( 𝐴 𝐿 𝑏 ) ) |
| 51 |
50 47
|
eqeltrrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → ( 𝐴 𝐿 𝑏 ) ∈ ran 𝐿 ) |
| 52 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) |
| 53 |
1 2 3 6 46 47 51 52
|
perpneq |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) ∧ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) → 𝐷 ≠ ( 𝐴 𝐿 𝑏 ) ) |
| 54 |
45 53
|
mtand |
⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) ∧ ¬ 𝐴 = 𝑏 ) → ¬ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) |
| 55 |
54
|
ex |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) → ( ¬ 𝐴 = 𝑏 → ¬ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) ) |
| 56 |
55
|
con4d |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) → 𝐴 = 𝑏 ) ) |
| 57 |
|
idd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) → ( 𝐴 = 𝑏 → 𝐴 = 𝑏 ) ) |
| 58 |
56 57
|
jaod |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) → ( ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) → 𝐴 = 𝑏 ) ) |
| 59 |
58
|
impr |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐴 = 𝑏 ) |
| 60 |
59
|
eqcomd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑏 = 𝐴 ) |
| 61 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → 𝑏 = 𝐴 ) |
| 62 |
61
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐴 ) ) |
| 63 |
1 2 3 4 5 8 8
|
midid |
⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐴 ) = 𝐴 ) |
| 64 |
63
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐴 ) = 𝐴 ) |
| 65 |
62 64
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = 𝐴 ) |
| 66 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → 𝐴 ∈ 𝐷 ) |
| 67 |
65 66
|
eqeltrd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) |
| 68 |
61
|
eqcomd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → 𝐴 = 𝑏 ) |
| 69 |
68
|
olcd |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) |
| 70 |
67 69
|
jca |
⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = 𝐴 ) → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 71 |
60 70
|
impbida |
⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = 𝐴 ) ) |
| 72 |
71
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) → ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = 𝐴 ) ) |
| 73 |
|
reu6i |
⊢ ( ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = 𝐴 ) ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 74 |
9 72 73
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 75 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐺 ∈ TarskiG ) |
| 76 |
75
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐺 ∈ TarskiG ) |
| 77 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 ) |
| 78 |
77
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ∈ ran 𝐿 ) |
| 79 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥 ∈ 𝐷 ) |
| 80 |
1 6 3 76 78 79
|
tglnpt |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥 ∈ 𝑃 ) |
| 81 |
|
eqid |
⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) |
| 82 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 ) |
| 83 |
82
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴 ∈ 𝑃 ) |
| 84 |
1 2 3 6 16 76 80 81 83
|
mircl |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ∈ 𝑃 ) |
| 85 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) → ( 𝐴 𝐿 𝑥 ) = ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ) |
| 86 |
85
|
breq1d |
⊢ ( 𝑥 = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) → ( ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ↔ ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ) |
| 87 |
|
simprl |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) |
| 88 |
|
simpr |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ¬ 𝐴 ∈ 𝐷 ) |
| 89 |
1 2 3 6 75 77 82 88
|
foot |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ∃! 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 90 |
|
reurmo |
⊢ ( ∃! 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 → ∃* 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 91 |
89 90
|
syl |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ∃* 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 92 |
91
|
ad4antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ∃* 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 93 |
79
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑥 ∈ 𝐷 ) |
| 94 |
|
simpllr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 95 |
76
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐺 ∈ TarskiG ) |
| 96 |
83
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐴 ∈ 𝑃 ) |
| 97 |
|
simplr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑏 ∈ 𝑃 ) |
| 98 |
5
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐺 DimTarskiG≥ 2 ) |
| 99 |
1 2 3 95 98 96 97
|
midcl |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑃 ) |
| 100 |
1 2 3 95 98 96 97
|
midbtwn |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐴 𝐼 𝑏 ) ) |
| 101 |
88
|
ad4antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ¬ 𝐴 ∈ 𝐷 ) |
| 102 |
|
nelne2 |
⊢ ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ≠ 𝐴 ) |
| 103 |
87 101 102
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ≠ 𝐴 ) |
| 104 |
1 2 3 95 96 99 97 100 103
|
tgbtwnne |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐴 ≠ 𝑏 ) |
| 105 |
1 3 6 95 96 97 99 104 100
|
btwnlng1 |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ ( 𝐴 𝐿 𝑏 ) ) |
| 106 |
1 3 6 95 96 97 104 99 103 105
|
tglineelsb2 |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 𝐿 𝑏 ) = ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ) |
| 107 |
78
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐷 ∈ ran 𝐿 ) |
| 108 |
1 3 6 95 96 97 104
|
tgelrnln |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 𝐿 𝑏 ) ∈ ran 𝐿 ) |
| 109 |
104
|
neneqd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ¬ 𝐴 = 𝑏 ) |
| 110 |
|
simprr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) |
| 111 |
110
|
orcomd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 = 𝑏 ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) ) |
| 112 |
111
|
ord |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( ¬ 𝐴 = 𝑏 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) ) |
| 113 |
109 112
|
mpd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) |
| 114 |
1 2 3 6 95 107 108 113
|
perpcom |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 𝐿 𝑏 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 115 |
106 114
|
eqbrtrrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 116 |
86 87 92 93 94 115
|
rmoi2 |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑥 = ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ) |
| 117 |
116
|
eqcomd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = 𝑥 ) |
| 118 |
80
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑥 ∈ 𝑃 ) |
| 119 |
1 2 3 95 98 96 97 16 118
|
ismidb |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → ( 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = 𝑥 ) ) |
| 120 |
117 119
|
mpbird |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) → 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) |
| 121 |
|
simpr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) |
| 122 |
76
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝐺 ∈ TarskiG ) |
| 123 |
5
|
ad5antr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝐺 DimTarskiG≥ 2 ) |
| 124 |
83
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝐴 ∈ 𝑃 ) |
| 125 |
|
simplr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝑏 ∈ 𝑃 ) |
| 126 |
80
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝑃 ) |
| 127 |
1 2 3 122 123 124 125 16 126
|
ismidb |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = 𝑥 ) ) |
| 128 |
121 127
|
mpbid |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) = 𝑥 ) |
| 129 |
79
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝐷 ) |
| 130 |
128 129
|
eqeltrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) |
| 131 |
122
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐺 ∈ TarskiG ) |
| 132 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 133 |
6 131 132
|
perpln1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → ( 𝐴 𝐿 𝑥 ) ∈ ran 𝐿 ) |
| 134 |
78
|
ad3antrrr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐷 ∈ ran 𝐿 ) |
| 135 |
1 2 3 6 131 133 134 132
|
perpcom |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) ) |
| 136 |
124
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐴 ∈ 𝑃 ) |
| 137 |
126
|
adantr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑥 ∈ 𝑃 ) |
| 138 |
1 3 6 131 136 137 133
|
tglnne |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐴 ≠ 𝑥 ) |
| 139 |
|
simpllr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑏 ∈ 𝑃 ) |
| 140 |
|
simpr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐴 ≠ 𝑏 ) |
| 141 |
140
|
necomd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑏 ≠ 𝐴 ) |
| 142 |
1 2 3 6 16 131 137 81 136
|
mirbtwn |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑥 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) 𝐼 𝐴 ) ) |
| 143 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) |
| 144 |
143
|
oveq1d |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → ( 𝑏 𝐼 𝐴 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) 𝐼 𝐴 ) ) |
| 145 |
142 144
|
eleqtrrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑥 ∈ ( 𝑏 𝐼 𝐴 ) ) |
| 146 |
1 3 6 131 139 136 137 141 145
|
btwnlng1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑥 ∈ ( 𝑏 𝐿 𝐴 ) ) |
| 147 |
1 3 6 131 136 137 139 138 146 141
|
lnrot1 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝑏 ∈ ( 𝐴 𝐿 𝑥 ) ) |
| 148 |
1 3 6 131 136 137 138 139 141 147
|
tglineelsb2 |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → ( 𝐴 𝐿 𝑥 ) = ( 𝐴 𝐿 𝑏 ) ) |
| 149 |
135 148
|
breqtrd |
⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ∧ 𝐴 ≠ 𝑏 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) |
| 150 |
149
|
ex |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( 𝐴 ≠ 𝑏 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ) ) |
| 151 |
150
|
necon1bd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( ¬ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) → 𝐴 = 𝑏 ) ) |
| 152 |
151
|
orrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) |
| 153 |
130 152
|
jca |
⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) ∧ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 154 |
120 153
|
impbida |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑏 ∈ 𝑃 ) → ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ) |
| 155 |
154
|
ralrimiva |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ) |
| 156 |
|
reu6i |
⊢ ( ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ∈ 𝑃 ∧ ∀ 𝑏 ∈ 𝑃 ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ↔ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐴 ) ) ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 157 |
84 155 156
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 158 |
1 2 3 6 75 77 82 88
|
footex |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) |
| 159 |
157 158
|
r19.29a |
⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |
| 160 |
74 159
|
pm2.61dan |
⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( ( 𝐴 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑏 ) ∨ 𝐴 = 𝑏 ) ) ) |