Metamath Proof Explorer

Theorem lmiisolem

Description: Lemma for lmiiso . (Contributed by Thierry Arnoux, 14-Dec-2019)

Ref Expression
Hypotheses ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismid.d ⊢ − = ( dist ‘ 𝐺 )
ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
lmif.m ⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
lmif.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
lmif.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
lmiiso.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
lmiiso.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lmiisolem.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 )
lmiisolem.z ⊢ 𝑍 = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
Assertion lmiisolem ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )

Proof

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 lmif.m ⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
7 lmif.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
8 lmif.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
9 lmiiso.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 lmiiso.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 lmiisolem.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 )
12 lmiisolem.z ⊢ 𝑍 = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝐺 ∈ TarskiG )
14 1 2 3 4 5 6 7 8 9 lmicl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
15 1 2 3 4 5 9 14 midcl ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
16 1 2 3 4 5 6 7 8 10 lmicl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
17 1 2 3 4 5 10 16 midcl ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝑃 )
18 1 2 3 4 5 15 17 midcl ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ∈ 𝑃 )
19 12 18 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝑍 ∈ 𝑃 )
21 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
22 1 2 3 7 21 4 19 11 9 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ 𝑃 )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑆 ‘ 𝐴 ) ∈ 𝑃 )
24 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝐴 ∈ 𝑃 )
25 1 2 3 7 21 13 20 11 24 mircgr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑍 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑍 − 𝐴 ) )
26 simpr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑆 ‘ 𝐴 ) = 𝑍 )
27 26 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝑍 = ( 𝑆 ‘ 𝐴 ) )
28 1 2 3 13 20 23 20 24 25 27 tgcgreq ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝑍 = 𝐴 )
29 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
31 12 30 eqtr4id ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
32 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
33 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝐺 DimTarskiG≥ 2 )
34 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
35 1 2 3 32 33 34 34 midid ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) )
36 31 35 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 = ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) )
37 eqidd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐴 ) )
38 1 2 3 4 5 6 7 8 9 14 islmib ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐴 ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) ) ) )
39 37 38 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) ) )
40 39 simpld ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 )
42 36 41 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 ∈ 𝐷 )
43 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
44 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
45 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝑃 )
46 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 ∈ 𝑃 )
47 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
48 1 2 3 4 5 15 17 midbtwn ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐼 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
49 12 48 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐼 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐼 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
51 1 3 7 43 44 45 46 47 50 btwnlng1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐿 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
52 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝐷 ∈ ran 𝐿 )
53 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 )
54 eqidd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ 𝐵 ) )
55 1 2 3 4 5 6 7 8 10 16 islmib ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ 𝐵 ) ↔ ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) ∨ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) ) ) )
56 54 55 mpbid ⊢ ( 𝜑 → ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) ∨ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) ) )
57 56 simpld ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝐷 )
58 57 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝐷 )
59 1 3 7 43 44 45 47 47 52 53 58 tglinethru ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝐷 = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐿 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
60 51 59 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) → 𝑍 ∈ 𝐷 )
61 42 60 pm2.61dane ⊢ ( 𝜑 → 𝑍 ∈ 𝐷 )
62 61 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝑍 ∈ 𝐷 )
63 28 62 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → 𝐴 ∈ 𝐷 )
64 1 2 3 4 5 6 7 8 9 lmiinv ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ 𝐷 ) )
65 64 biimpar ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝐷 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
66 63 65 syldan ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
67 66 28 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑀 ‘ 𝐴 ) = 𝑍 )
68 67 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) = ( 𝑍 − ( 𝑀 ‘ 𝐵 ) ) )
69 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝑍 = 𝑍 )
70 4 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐺 ∈ TarskiG )
71 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ∈ 𝑃 )
72 17 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝑃 )
73 1 2 3 4 5 10 16 midbtwn ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ ( 𝐵 𝐼 ( 𝑀 ‘ 𝐵 ) ) )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ ( 𝐵 𝐼 ( 𝑀 ‘ 𝐵 ) ) )
75 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐵 = ( 𝑀 ‘ 𝐵 ) )
76 75 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 𝐼 𝐵 ) = ( 𝐵 𝐼 ( 𝑀 ‘ 𝐵 ) ) )
77 74 76 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ ( 𝐵 𝐼 𝐵 ) )
78 1 2 3 70 71 72 77 axtgbtwnid ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐵 = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
79 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐵 = 𝐵 )
80 69 78 79 s3eqd ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ⟨“ 𝑍 𝐵 𝐵 ”⟩ = ⟨“ 𝑍 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐵 ”⟩ )
81 1 2 3 7 21 4 19 10 10 ragtrivb ⊢ ( 𝜑 → ⟨“ 𝑍 𝐵 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ⟨“ 𝑍 𝐵 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
83 80 82 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → ⟨“ 𝑍 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
84 4 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝐺 ∈ TarskiG )
85 61 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝑍 ∈ 𝐷 )
86 57 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝐷 )
87 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ∈ 𝑃 )
88 df-ne ⊢ ( 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ↔ ¬ 𝐵 = ( 𝑀 ‘ 𝐵 ) )
89 56 simprd ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) ∨ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) )
90 89 orcomd ⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐵 ) ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) ) )
91 90 orcanai ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) )
92 88 91 sylan2b ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) )
93 16 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
94 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) )
95 17 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ 𝑃 )
96 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → 𝐺 ∈ TarskiG )
97 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → 𝐵 ∈ 𝑃 )
98 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
99 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → 𝐺 DimTarskiG≥ 2 )
100 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 )
101 1 2 3 96 99 97 98 100 midcgr ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → ( 𝐵 − 𝐵 ) = ( 𝐵 − ( 𝑀 ‘ 𝐵 ) ) )
102 101 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → ( 𝐵 − ( 𝑀 ‘ 𝐵 ) ) = ( 𝐵 − 𝐵 ) )
103 1 2 3 96 97 98 97 102 axtgcgrid ⊢ ( ( 𝜑 ∧ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 ) → 𝐵 = ( 𝑀 ‘ 𝐵 ) )
104 103 ex ⊢ ( 𝜑 → ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = 𝐵 → 𝐵 = ( 𝑀 ‘ 𝐵 ) ) )
105 104 necon3d ⊢ ( 𝜑 → ( 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ≠ 𝐵 ) )
106 105 imp ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ≠ 𝐵 )
107 73 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ ( 𝐵 𝐼 ( 𝑀 ‘ 𝐵 ) ) )
108 1 3 7 84 87 93 95 94 107 btwnlng1 ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ∈ ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) )
109 1 3 7 84 87 93 94 95 106 108 tglineelsb2 ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) = ( 𝐵 𝐿 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
110 1 3 7 84 95 87 106 tglinecom ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐿 𝐵 ) = ( 𝐵 𝐿 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
111 109 110 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ( 𝐵 𝐿 ( 𝑀 ‘ 𝐵 ) ) = ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐿 𝐵 ) )
112 92 111 breqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐿 𝐵 ) )
113 1 2 3 7 84 85 86 87 112 perpdrag ⊢ ( ( 𝜑 ∧ 𝐵 ≠ ( 𝑀 ‘ 𝐵 ) ) → ⟨“ 𝑍 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
114 83 113 pm2.61dane ⊢ ( 𝜑 → ⟨“ 𝑍 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
115 1 2 3 7 21 4 19 17 10 israg ⊢ ( 𝜑 → ( ⟨“ 𝑍 ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) 𝐵 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑍 − 𝐵 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) ) ) )
116 114 115 mpbid ⊢ ( 𝜑 → ( 𝑍 − 𝐵 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) ) )
117 eqidd ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
118 1 2 3 4 5 10 16 21 17 ismidb ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) ↔ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
119 117 118 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) )
120 119 oveq2d ⊢ ( 𝜑 → ( 𝑍 − ( 𝑀 ‘ 𝐵 ) ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) ) )
121 116 120 eqtr4d ⊢ ( 𝜑 → ( 𝑍 − 𝐵 ) = ( 𝑍 − ( 𝑀 ‘ 𝐵 ) ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑍 − 𝐵 ) = ( 𝑍 − ( 𝑀 ‘ 𝐵 ) ) )
123 28 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( 𝑍 − 𝐵 ) = ( 𝐴 − 𝐵 ) )
124 68 122 123 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) = 𝑍 ) → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
125 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐺 ∈ TarskiG )
126 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑆 ‘ 𝐴 ) ∈ 𝑃 )
127 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝑍 ∈ 𝑃 )
128 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ∈ 𝑃 )
129 1 2 3 7 21 4 19 11 14 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
130 129 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
131 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
132 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐵 ∈ 𝑃 )
133 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
134 simpr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 )
135 1 2 3 7 21 125 127 11 128 mirbtwn ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝑍 ∈ ( ( 𝑆 ‘ 𝐴 ) 𝐼 𝐴 ) )
136 1 2 3 7 21 125 127 11 131 mirbtwn ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → 𝑍 ∈ ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
137 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝑍 = 𝑍 )
138 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐺 ∈ TarskiG )
139 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐴 ∈ 𝑃 )
140 15 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
141 1 2 3 4 5 9 14 midbtwn ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
143 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐴 = ( 𝑀 ‘ 𝐴 ) )
144 143 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 𝐼 𝐴 ) = ( 𝐴 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
145 142 144 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐼 𝐴 ) )
146 1 2 3 138 139 140 145 axtgbtwnid ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐴 = ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) )
147 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐴 = 𝐴 )
148 137 146 147 s3eqd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ⟨“ 𝑍 𝐴 𝐴 ”⟩ = ⟨“ 𝑍 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐴 ”⟩ )
149 1 2 3 7 21 4 19 9 9 ragtrivb ⊢ ( 𝜑 → ⟨“ 𝑍 𝐴 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
150 149 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ⟨“ 𝑍 𝐴 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
151 148 150 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → ⟨“ 𝑍 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
152 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝐺 ∈ TarskiG )
153 61 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝑍 ∈ 𝐷 )
154 40 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝐷 )
155 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝐴 ∈ 𝑃 )
156 df-ne ⊢ ( 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ↔ ¬ 𝐴 = ( 𝑀 ‘ 𝐴 ) )
157 39 simprd ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ∨ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) )
158 157 orcomd ⊢ ( 𝜑 → ( 𝐴 = ( 𝑀 ‘ 𝐴 ) ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) ) )
159 158 orcanai ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ( 𝑀 ‘ 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) )
160 156 159 sylan2b ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) )
161 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
162 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) )
163 15 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ 𝑃 )
164 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → 𝐺 ∈ TarskiG )
165 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → 𝐴 ∈ 𝑃 )
166 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
167 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → 𝐺 DimTarskiG≥ 2 )
168 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )
169 1 2 3 164 167 165 166 168 midcgr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → ( 𝐴 − 𝐴 ) = ( 𝐴 − ( 𝑀 ‘ 𝐴 ) ) )
170 169 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → ( 𝐴 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝐴 − 𝐴 ) )
171 1 2 3 164 165 166 165 170 axtgcgrid ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) → 𝐴 = ( 𝑀 ‘ 𝐴 ) )
172 171 ex ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = 𝐴 → 𝐴 = ( 𝑀 ‘ 𝐴 ) ) )
173 172 necon3d ⊢ ( 𝜑 → ( 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ 𝐴 ) )
174 173 imp ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ≠ 𝐴 )
175 141 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐼 ( 𝑀 ‘ 𝐴 ) ) )
176 1 3 7 152 155 161 163 162 175 btwnlng1 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ∈ ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) )
177 1 3 7 152 155 161 162 163 174 176 tglineelsb2 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) = ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
178 1 3 7 152 163 155 174 tglinecom ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐿 𝐴 ) = ( 𝐴 𝐿 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
179 177 178 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ( 𝐴 𝐿 ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐿 𝐴 ) )
180 160 179 breqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐿 𝐴 ) )
181 1 2 3 7 152 153 154 155 180 perpdrag ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝑀 ‘ 𝐴 ) ) → ⟨“ 𝑍 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
182 151 181 pm2.61dane ⊢ ( 𝜑 → ⟨“ 𝑍 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
183 1 2 3 7 21 4 19 15 9 israg ⊢ ( 𝜑 → ( ⟨“ 𝑍 ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝑍 − 𝐴 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ‘ 𝐴 ) ) ) )
184 182 183 mpbid ⊢ ( 𝜑 → ( 𝑍 − 𝐴 ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ‘ 𝐴 ) ) )
185 eqidd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) )
186 1 2 3 4 5 9 14 21 15 ismidb ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
187 185 186 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ‘ 𝐴 ) )
188 187 oveq2d ⊢ ( 𝜑 → ( 𝑍 − ( 𝑀 ‘ 𝐴 ) ) = ( 𝑍 − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ‘ 𝐴 ) ) )
189 184 188 eqtr4d ⊢ ( 𝜑 → ( 𝑍 − 𝐴 ) = ( 𝑍 − ( 𝑀 ‘ 𝐴 ) ) )
190 1 2 3 7 21 4 19 11 9 mircgr ⊢ ( 𝜑 → ( 𝑍 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑍 − 𝐴 ) )
191 1 2 3 7 21 4 19 11 14 mircgr ⊢ ( 𝜑 → ( 𝑍 − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑍 − ( 𝑀 ‘ 𝐴 ) ) )
192 189 190 191 3eqtr4d ⊢ ( 𝜑 → ( 𝑍 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑍 − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
193 192 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑍 − ( 𝑆 ‘ 𝐴 ) ) = ( 𝑍 − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
194 1 2 3 125 127 126 127 130 193 tgcgrcomlr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( ( 𝑆 ‘ 𝐴 ) − 𝑍 ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) − 𝑍 ) )
195 189 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑍 − 𝐴 ) = ( 𝑍 − ( 𝑀 ‘ 𝐴 ) ) )
196 11 fveq1i ⊢ ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) )
197 1 2 3 4 5 9 14 11 19 mirmid ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
198 12 eqcomi ⊢ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) = 𝑍
199 1 2 3 4 5 15 17 21 19 ismidb ⊢ ( 𝜑 → ( ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ( midG ‘ 𝐺 ) ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) = 𝑍 ) )
200 198 199 mpbiri ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑍 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐴 ) ) ) )
201 196 197 200 3eqtr4a ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
202 1 2 3 4 5 22 129 21 17 ismidb ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) )
203 201 202 mpbird ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) )
204 119 203 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐵 ) − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) ) )
205 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) )
206 1 2 3 7 21 4 17 205 10 22 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ 𝐵 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) ( 𝑀 ‘ 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) ) = ( 𝐵 − ( 𝑆 ‘ 𝐴 ) ) )
207 204 206 eqtr2d ⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ 𝐵 ) − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝐵 − ( 𝑆 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ 𝐵 ) − ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
209 1 2 3 125 132 126 133 130 208 tgcgrcomlr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( ( 𝑆 ‘ 𝐴 ) − 𝐵 ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐴 ) ) − ( 𝑀 ‘ 𝐵 ) ) )
210 121 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝑍 − 𝐵 ) = ( 𝑍 − ( 𝑀 ‘ 𝐵 ) ) )
211 1 2 3 125 126 127 128 130 127 131 132 133 134 135 136 194 195 209 210 axtg5seg ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( 𝐴 − 𝐵 ) = ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) )
212 211 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐴 ) ≠ 𝑍 ) → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
213 124 212 pm2.61dane ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐵 ) ) = ( 𝐴 − 𝐵 ) )