MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmiisolem Structured version   Visualization version   GIF version

Theorem lmiisolem 28047
Description: Lemma for lmiiso 28048. (Contributed by Thierry Arnoux, 14-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
lmiisolem (πœ‘ β†’ ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)) = (𝐴 βˆ’ 𝐡))

Proof of Theorem lmiisolem
StepHypRef Expression
1 ismid.p . . . . . . . 8 𝑃 = (Baseβ€˜πΊ)
2 ismid.d . . . . . . . 8 βˆ’ = (distβ€˜πΊ)
3 ismid.i . . . . . . . 8 𝐼 = (Itvβ€˜πΊ)
4 ismid.g . . . . . . . . 9 (πœ‘ β†’ 𝐺 ∈ TarskiG)
54adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝐺 ∈ TarskiG)
6 lmiisolem.z . . . . . . . . . 10 𝑍 = ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
7 ismid.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝐺DimTarskiGβ‰₯2)
8 lmiiso.1 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ 𝑃)
9 lmif.m . . . . . . . . . . . . 13 𝑀 = ((lInvGβ€˜πΊ)β€˜π·)
10 lmif.l . . . . . . . . . . . . 13 𝐿 = (LineGβ€˜πΊ)
11 lmif.d . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ ran 𝐿)
121, 2, 3, 4, 7, 9, 10, 11, 8lmicl 28037 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘€β€˜π΄) ∈ 𝑃)
131, 2, 3, 4, 7, 8, 12midcl 28028 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝑃)
14 lmiiso.2 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ 𝑃)
151, 2, 3, 4, 7, 9, 10, 11, 14lmicl 28037 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘€β€˜π΅) ∈ 𝑃)
161, 2, 3, 4, 7, 14, 15midcl 28028 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝑃)
171, 2, 3, 4, 7, 13, 16midcl 28028 . . . . . . . . . 10 (πœ‘ β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) ∈ 𝑃)
186, 17eqeltrid 2838 . . . . . . . . 9 (πœ‘ β†’ 𝑍 ∈ 𝑃)
1918adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝑍 ∈ 𝑃)
20 eqid 2733 . . . . . . . . . 10 (pInvGβ€˜πΊ) = (pInvGβ€˜πΊ)
21 lmiisolem.s . . . . . . . . . 10 𝑆 = ((pInvGβ€˜πΊ)β€˜π‘)
221, 2, 3, 10, 20, 4, 18, 21, 8mircl 27912 . . . . . . . . 9 (πœ‘ β†’ (π‘†β€˜π΄) ∈ 𝑃)
2322adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (π‘†β€˜π΄) ∈ 𝑃)
248adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝐴 ∈ 𝑃)
251, 2, 3, 10, 20, 5, 19, 21, 24mircgr 27908 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (𝑍 βˆ’ (π‘†β€˜π΄)) = (𝑍 βˆ’ 𝐴))
26 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (π‘†β€˜π΄) = 𝑍)
2726eqcomd 2739 . . . . . . . 8 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝑍 = (π‘†β€˜π΄))
281, 2, 3, 5, 19, 23, 19, 24, 25, 27tgcgreq 27733 . . . . . . 7 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝑍 = 𝐴)
29 simpr 486 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
3029oveq2d 7425 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))) = ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
316, 30eqtr4id 2792 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 = ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
324adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝐺 ∈ TarskiG)
337adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝐺DimTarskiGβ‰₯2)
3413adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝑃)
351, 2, 3, 32, 33, 34, 34midid 28032 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))) = (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))
3631, 35eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 = (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))
37 eqidd 2734 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜π΄) = (π‘€β€˜π΄))
381, 2, 3, 4, 7, 9, 10, 11, 8, 12islmib 28038 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘€β€˜π΄) = (π‘€β€˜π΄) ↔ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷 ∧ (𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄)) ∨ 𝐴 = (π‘€β€˜π΄)))))
3937, 38mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷 ∧ (𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄)) ∨ 𝐴 = (π‘€β€˜π΄))))
4039simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷)
4140adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷)
4236, 41eqeltrd 2834 . . . . . . . . 9 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 ∈ 𝐷)
434adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝐺 ∈ TarskiG)
4413adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝑃)
4516adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝑃)
4618adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 ∈ 𝑃)
47 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
481, 2, 3, 4, 7, 13, 16midbtwn 28030 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) ∈ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐼(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
496, 48eqeltrid 2838 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑍 ∈ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐼(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
5049adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 ∈ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐼(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
511, 3, 10, 43, 44, 45, 46, 47, 50btwnlng1 27870 . . . . . . . . . 10 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 ∈ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐿(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
5211adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝐷 ∈ ran 𝐿)
5340adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷)
54 eqidd 2734 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘€β€˜π΅) = (π‘€β€˜π΅))
551, 2, 3, 4, 7, 9, 10, 11, 14, 15islmib 28038 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘€β€˜π΅) = (π‘€β€˜π΅) ↔ ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝐷 ∧ (𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅)) ∨ 𝐡 = (π‘€β€˜π΅)))))
5654, 55mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝐷 ∧ (𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅)) ∨ 𝐡 = (π‘€β€˜π΅))))
5756simpld 496 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝐷)
5857adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝐷)
591, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58tglinethru 27887 . . . . . . . . . 10 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝐷 = ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐿(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
6051, 59eleqtrrd 2837 . . . . . . . . 9 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) β†’ 𝑍 ∈ 𝐷)
6142, 60pm2.61dane 3030 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ 𝐷)
6261adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝑍 ∈ 𝐷)
6328, 62eqeltrrd 2835 . . . . . 6 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ 𝐴 ∈ 𝐷)
641, 2, 3, 4, 7, 9, 10, 11, 8lmiinv 28043 . . . . . . 7 (πœ‘ β†’ ((π‘€β€˜π΄) = 𝐴 ↔ 𝐴 ∈ 𝐷))
6564biimpar 479 . . . . . 6 ((πœ‘ ∧ 𝐴 ∈ 𝐷) β†’ (π‘€β€˜π΄) = 𝐴)
6663, 65syldan 592 . . . . 5 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (π‘€β€˜π΄) = 𝐴)
6766, 28eqtr4d 2776 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (π‘€β€˜π΄) = 𝑍)
6867oveq1d 7424 . . 3 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)) = (𝑍 βˆ’ (π‘€β€˜π΅)))
69 eqidd 2734 . . . . . . . . 9 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝑍 = 𝑍)
704adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐺 ∈ TarskiG)
7114adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐡 ∈ 𝑃)
7216adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝑃)
731, 2, 3, 4, 7, 14, 15midbtwn 28030 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ (𝐡𝐼(π‘€β€˜π΅)))
7473adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ (𝐡𝐼(π‘€β€˜π΅)))
75 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐡 = (π‘€β€˜π΅))
7675oveq2d 7425 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ (𝐡𝐼𝐡) = (𝐡𝐼(π‘€β€˜π΅)))
7774, 76eleqtrrd 2837 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ (𝐡𝐼𝐡))
781, 2, 3, 70, 71, 72, 77axtgbtwnid 27717 . . . . . . . . 9 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐡 = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
79 eqidd 2734 . . . . . . . . 9 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐡 = 𝐡)
8069, 78, 79s3eqd 14815 . . . . . . . 8 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ βŸ¨β€œπ‘π΅π΅β€βŸ© = βŸ¨β€œπ‘(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))π΅β€βŸ©)
811, 2, 3, 10, 20, 4, 18, 14, 14ragtrivb 27953 . . . . . . . . 9 (πœ‘ β†’ βŸ¨β€œπ‘π΅π΅β€βŸ© ∈ (∟Gβ€˜πΊ))
8281adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ βŸ¨β€œπ‘π΅π΅β€βŸ© ∈ (∟Gβ€˜πΊ))
8380, 82eqeltrrd 2835 . . . . . . 7 ((πœ‘ ∧ 𝐡 = (π‘€β€˜π΅)) β†’ βŸ¨β€œπ‘(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))π΅β€βŸ© ∈ (∟Gβ€˜πΊ))
844adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝐺 ∈ TarskiG)
8561adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝑍 ∈ 𝐷)
8657adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝐷)
8714adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝐡 ∈ 𝑃)
88 df-ne 2942 . . . . . . . . . 10 (𝐡 β‰  (π‘€β€˜π΅) ↔ Β¬ 𝐡 = (π‘€β€˜π΅))
8956simprd 497 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅)) ∨ 𝐡 = (π‘€β€˜π΅)))
9089orcomd 870 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 = (π‘€β€˜π΅) ∨ 𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅))))
9190orcanai 1002 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐡 = (π‘€β€˜π΅)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅)))
9288, 91sylan2b 595 . . . . . . . . 9 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)(𝐡𝐿(π‘€β€˜π΅)))
9315adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (π‘€β€˜π΅) ∈ 𝑃)
94 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝐡 β‰  (π‘€β€˜π΅))
9516adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ 𝑃)
964adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ 𝐺 ∈ TarskiG)
9714adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ 𝐡 ∈ 𝑃)
9815adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ (π‘€β€˜π΅) ∈ 𝑃)
997adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ 𝐺DimTarskiGβ‰₯2)
100 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡)
1011, 2, 3, 96, 99, 97, 98, 100midcgr 28031 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ (𝐡 βˆ’ 𝐡) = (𝐡 βˆ’ (π‘€β€˜π΅)))
102101eqcomd 2739 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ (𝐡 βˆ’ (π‘€β€˜π΅)) = (𝐡 βˆ’ 𝐡))
1031, 2, 3, 96, 97, 98, 97, 102axtgcgrid 27714 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡) β†’ 𝐡 = (π‘€β€˜π΅))
104103ex 414 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = 𝐡 β†’ 𝐡 = (π‘€β€˜π΅)))
105104necon3d 2962 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 β‰  (π‘€β€˜π΅) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) β‰  𝐡))
106105imp 408 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) β‰  𝐡)
10773adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ (𝐡𝐼(π‘€β€˜π΅)))
1081, 3, 10, 84, 87, 93, 95, 94, 107btwnlng1 27870 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) ∈ (𝐡𝐿(π‘€β€˜π΅)))
1091, 3, 10, 84, 87, 93, 94, 95, 106, 108tglineelsb2 27883 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡𝐿(π‘€β€˜π΅)) = (𝐡𝐿(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
1101, 3, 10, 84, 95, 87, 106tglinecom 27886 . . . . . . . . . 10 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))𝐿𝐡) = (𝐡𝐿(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
111109, 110eqtr4d 2776 . . . . . . . . 9 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ (𝐡𝐿(π‘€β€˜π΅)) = ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))𝐿𝐡))
11292, 111breqtrd 5175 . . . . . . . 8 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))𝐿𝐡))
1131, 2, 3, 10, 84, 85, 86, 87, 112perpdrag 27979 . . . . . . 7 ((πœ‘ ∧ 𝐡 β‰  (π‘€β€˜π΅)) β†’ βŸ¨β€œπ‘(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))π΅β€βŸ© ∈ (∟Gβ€˜πΊ))
11483, 113pm2.61dane 3030 . . . . . 6 (πœ‘ β†’ βŸ¨β€œπ‘(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))π΅β€βŸ© ∈ (∟Gβ€˜πΊ))
1151, 2, 3, 10, 20, 4, 18, 16, 14israg 27948 . . . . . 6 (πœ‘ β†’ (βŸ¨β€œπ‘(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))π΅β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝑍 βˆ’ 𝐡) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅))))
116114, 115mpbid 231 . . . . 5 (πœ‘ β†’ (𝑍 βˆ’ 𝐡) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅)))
117 eqidd 2734 . . . . . . 7 (πœ‘ β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
1181, 2, 3, 4, 7, 14, 15, 20, 16ismidb 28029 . . . . . . 7 (πœ‘ β†’ ((π‘€β€˜π΅) = (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅) ↔ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
119117, 118mpbird 257 . . . . . 6 (πœ‘ β†’ (π‘€β€˜π΅) = (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅))
120119oveq2d 7425 . . . . 5 (πœ‘ β†’ (𝑍 βˆ’ (π‘€β€˜π΅)) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅)))
121116, 120eqtr4d 2776 . . . 4 (πœ‘ β†’ (𝑍 βˆ’ 𝐡) = (𝑍 βˆ’ (π‘€β€˜π΅)))
122121adantr 482 . . 3 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (𝑍 βˆ’ 𝐡) = (𝑍 βˆ’ (π‘€β€˜π΅)))
12328oveq1d 7424 . . 3 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ (𝑍 βˆ’ 𝐡) = (𝐴 βˆ’ 𝐡))
12468, 122, 1233eqtr2d 2779 . 2 ((πœ‘ ∧ (π‘†β€˜π΄) = 𝑍) β†’ ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)) = (𝐴 βˆ’ 𝐡))
1254adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝐺 ∈ TarskiG)
12622adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (π‘†β€˜π΄) ∈ 𝑃)
12718adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝑍 ∈ 𝑃)
1288adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝐴 ∈ 𝑃)
1291, 2, 3, 10, 20, 4, 18, 21, 12mircl 27912 . . . . 5 (πœ‘ β†’ (π‘†β€˜(π‘€β€˜π΄)) ∈ 𝑃)
130129adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (π‘†β€˜(π‘€β€˜π΄)) ∈ 𝑃)
13112adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (π‘€β€˜π΄) ∈ 𝑃)
13214adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝐡 ∈ 𝑃)
13315adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (π‘€β€˜π΅) ∈ 𝑃)
134 simpr 486 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (π‘†β€˜π΄) β‰  𝑍)
1351, 2, 3, 10, 20, 125, 127, 21, 128mirbtwn 27909 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝑍 ∈ ((π‘†β€˜π΄)𝐼𝐴))
1361, 2, 3, 10, 20, 125, 127, 21, 131mirbtwn 27909 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ 𝑍 ∈ ((π‘†β€˜(π‘€β€˜π΄))𝐼(π‘€β€˜π΄)))
137 eqidd 2734 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝑍 = 𝑍)
1384adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐺 ∈ TarskiG)
1398adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐴 ∈ 𝑃)
14013adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝑃)
1411, 2, 3, 4, 7, 8, 12midbtwn 28030 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ (𝐴𝐼(π‘€β€˜π΄)))
142141adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ (𝐴𝐼(π‘€β€˜π΄)))
143 simpr 486 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐴 = (π‘€β€˜π΄))
144143oveq2d 7425 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ (𝐴𝐼𝐴) = (𝐴𝐼(π‘€β€˜π΄)))
145142, 144eleqtrrd 2837 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ (𝐴𝐼𝐴))
1461, 2, 3, 138, 139, 140, 145axtgbtwnid 27717 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐴 = (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))
147 eqidd 2734 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐴 = 𝐴)
148137, 146, 147s3eqd 14815 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ βŸ¨β€œπ‘π΄π΄β€βŸ© = βŸ¨β€œπ‘(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))π΄β€βŸ©)
1491, 2, 3, 10, 20, 4, 18, 8, 8ragtrivb 27953 . . . . . . . . . . . 12 (πœ‘ β†’ βŸ¨β€œπ‘π΄π΄β€βŸ© ∈ (∟Gβ€˜πΊ))
150149adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ βŸ¨β€œπ‘π΄π΄β€βŸ© ∈ (∟Gβ€˜πΊ))
151148, 150eqeltrrd 2835 . . . . . . . . . 10 ((πœ‘ ∧ 𝐴 = (π‘€β€˜π΄)) β†’ βŸ¨β€œπ‘(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))π΄β€βŸ© ∈ (∟Gβ€˜πΊ))
1524adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝐺 ∈ TarskiG)
15361adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝑍 ∈ 𝐷)
15440adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝐷)
1558adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝐴 ∈ 𝑃)
156 df-ne 2942 . . . . . . . . . . . . 13 (𝐴 β‰  (π‘€β€˜π΄) ↔ Β¬ 𝐴 = (π‘€β€˜π΄))
15739simprd 497 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄)) ∨ 𝐴 = (π‘€β€˜π΄)))
158157orcomd 870 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐴 = (π‘€β€˜π΄) ∨ 𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄))))
159158orcanai 1002 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝐴 = (π‘€β€˜π΄)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄)))
160156, 159sylan2b 595 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)(𝐴𝐿(π‘€β€˜π΄)))
16112adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (π‘€β€˜π΄) ∈ 𝑃)
162 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝐴 β‰  (π‘€β€˜π΄))
16313adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ 𝑃)
1644adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ 𝐺 ∈ TarskiG)
1658adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ 𝐴 ∈ 𝑃)
16612adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ (π‘€β€˜π΄) ∈ 𝑃)
1677adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ 𝐺DimTarskiGβ‰₯2)
168 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴)
1691, 2, 3, 164, 167, 165, 166, 168midcgr 28031 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ (𝐴 βˆ’ 𝐴) = (𝐴 βˆ’ (π‘€β€˜π΄)))
170169eqcomd 2739 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ (𝐴 βˆ’ (π‘€β€˜π΄)) = (𝐴 βˆ’ 𝐴))
1711, 2, 3, 164, 165, 166, 165, 170axtgcgrid 27714 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴) β†’ 𝐴 = (π‘€β€˜π΄))
172171ex 414 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = 𝐴 β†’ 𝐴 = (π‘€β€˜π΄)))
173172necon3d 2962 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴 β‰  (π‘€β€˜π΄) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  𝐴))
174173imp 408 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) β‰  𝐴)
175141adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ (𝐴𝐼(π‘€β€˜π΄)))
1761, 3, 10, 152, 155, 161, 163, 162, 175btwnlng1 27870 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) ∈ (𝐴𝐿(π‘€β€˜π΄)))
1771, 3, 10, 152, 155, 161, 162, 163, 174, 176tglineelsb2 27883 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴𝐿(π‘€β€˜π΄)) = (𝐴𝐿(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
1781, 3, 10, 152, 163, 155, 174tglinecom 27886 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐿𝐴) = (𝐴𝐿(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
179177, 178eqtr4d 2776 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ (𝐴𝐿(π‘€β€˜π΄)) = ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐿𝐴))
180160, 179breqtrd 5175 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ 𝐷(βŸ‚Gβ€˜πΊ)((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))𝐿𝐴))
1811, 2, 3, 10, 152, 153, 154, 155, 180perpdrag 27979 . . . . . . . . . 10 ((πœ‘ ∧ 𝐴 β‰  (π‘€β€˜π΄)) β†’ βŸ¨β€œπ‘(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))π΄β€βŸ© ∈ (∟Gβ€˜πΊ))
182151, 181pm2.61dane 3030 . . . . . . . . 9 (πœ‘ β†’ βŸ¨β€œπ‘(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))π΄β€βŸ© ∈ (∟Gβ€˜πΊ))
1831, 2, 3, 10, 20, 4, 18, 13, 8israg 27948 . . . . . . . . 9 (πœ‘ β†’ (βŸ¨β€œπ‘(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))π΄β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝑍 βˆ’ 𝐴) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))β€˜π΄))))
184182, 183mpbid 231 . . . . . . . 8 (πœ‘ β†’ (𝑍 βˆ’ 𝐴) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))β€˜π΄)))
185 eqidd 2734 . . . . . . . . . 10 (πœ‘ β†’ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))
1861, 2, 3, 4, 7, 8, 12, 20, 13ismidb 28029 . . . . . . . . . 10 (πœ‘ β†’ ((π‘€β€˜π΄) = (((pInvGβ€˜πΊ)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))β€˜π΄) ↔ (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)) = (𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
187185, 186mpbird 257 . . . . . . . . 9 (πœ‘ β†’ (π‘€β€˜π΄) = (((pInvGβ€˜πΊ)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))β€˜π΄))
188187oveq2d 7425 . . . . . . . 8 (πœ‘ β†’ (𝑍 βˆ’ (π‘€β€˜π΄)) = (𝑍 βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))β€˜π΄)))
189184, 188eqtr4d 2776 . . . . . . 7 (πœ‘ β†’ (𝑍 βˆ’ 𝐴) = (𝑍 βˆ’ (π‘€β€˜π΄)))
1901, 2, 3, 10, 20, 4, 18, 21, 8mircgr 27908 . . . . . . 7 (πœ‘ β†’ (𝑍 βˆ’ (π‘†β€˜π΄)) = (𝑍 βˆ’ 𝐴))
1911, 2, 3, 10, 20, 4, 18, 21, 12mircgr 27908 . . . . . . 7 (πœ‘ β†’ (𝑍 βˆ’ (π‘†β€˜(π‘€β€˜π΄))) = (𝑍 βˆ’ (π‘€β€˜π΄)))
192189, 190, 1913eqtr4d 2783 . . . . . 6 (πœ‘ β†’ (𝑍 βˆ’ (π‘†β€˜π΄)) = (𝑍 βˆ’ (π‘†β€˜(π‘€β€˜π΄))))
193192adantr 482 . . . . 5 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (𝑍 βˆ’ (π‘†β€˜π΄)) = (𝑍 βˆ’ (π‘†β€˜(π‘€β€˜π΄))))
1941, 2, 3, 125, 127, 126, 127, 130, 193tgcgrcomlr 27731 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ ((π‘†β€˜π΄) βˆ’ 𝑍) = ((π‘†β€˜(π‘€β€˜π΄)) βˆ’ 𝑍))
195189adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (𝑍 βˆ’ 𝐴) = (𝑍 βˆ’ (π‘€β€˜π΄)))
19621fveq1i 6893 . . . . . . . . . 10 (π‘†β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))) = (((pInvGβ€˜πΊ)β€˜π‘)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄)))
1971, 2, 3, 4, 7, 8, 12, 21, 18mirmid 28034 . . . . . . . . . 10 (πœ‘ β†’ ((π‘†β€˜π΄)(midGβ€˜πΊ)(π‘†β€˜(π‘€β€˜π΄))) = (π‘†β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
1986eqcomi 2742 . . . . . . . . . . 11 ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) = 𝑍
1991, 2, 3, 4, 7, 13, 16, 20, 18ismidb 28029 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = (((pInvGβ€˜πΊ)β€˜π‘)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))) ↔ ((𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))(midGβ€˜πΊ)(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) = 𝑍))
200198, 199mpbiri 258 . . . . . . . . . 10 (πœ‘ β†’ (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)) = (((pInvGβ€˜πΊ)β€˜π‘)β€˜(𝐴(midGβ€˜πΊ)(π‘€β€˜π΄))))
201196, 197, 2003eqtr4a 2799 . . . . . . . . 9 (πœ‘ β†’ ((π‘†β€˜π΄)(midGβ€˜πΊ)(π‘†β€˜(π‘€β€˜π΄))) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
2021, 2, 3, 4, 7, 22, 129, 20, 16ismidb 28029 . . . . . . . . 9 (πœ‘ β†’ ((π‘†β€˜(π‘€β€˜π΄)) = (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜(π‘†β€˜π΄)) ↔ ((π‘†β€˜π΄)(midGβ€˜πΊ)(π‘†β€˜(π‘€β€˜π΄))) = (𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))))
203201, 202mpbird 257 . . . . . . . 8 (πœ‘ β†’ (π‘†β€˜(π‘€β€˜π΄)) = (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜(π‘†β€˜π΄)))
204119, 203oveq12d 7427 . . . . . . 7 (πœ‘ β†’ ((π‘€β€˜π΅) βˆ’ (π‘†β€˜(π‘€β€˜π΄))) = ((((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅) βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜(π‘†β€˜π΄))))
205 eqid 2733 . . . . . . . 8 ((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅))) = ((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))
2061, 2, 3, 10, 20, 4, 16, 205, 14, 22miriso 27921 . . . . . . 7 (πœ‘ β†’ ((((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜π΅) βˆ’ (((pInvGβ€˜πΊ)β€˜(𝐡(midGβ€˜πΊ)(π‘€β€˜π΅)))β€˜(π‘†β€˜π΄))) = (𝐡 βˆ’ (π‘†β€˜π΄)))
207204, 206eqtr2d 2774 . . . . . 6 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜π΄)) = ((π‘€β€˜π΅) βˆ’ (π‘†β€˜(π‘€β€˜π΄))))
208207adantr 482 . . . . 5 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (𝐡 βˆ’ (π‘†β€˜π΄)) = ((π‘€β€˜π΅) βˆ’ (π‘†β€˜(π‘€β€˜π΄))))
2091, 2, 3, 125, 132, 126, 133, 130, 208tgcgrcomlr 27731 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ ((π‘†β€˜π΄) βˆ’ 𝐡) = ((π‘†β€˜(π‘€β€˜π΄)) βˆ’ (π‘€β€˜π΅)))
210121adantr 482 . . . 4 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (𝑍 βˆ’ 𝐡) = (𝑍 βˆ’ (π‘€β€˜π΅)))
2111, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210axtg5seg 27716 . . 3 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ (𝐴 βˆ’ 𝐡) = ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)))
212211eqcomd 2739 . 2 ((πœ‘ ∧ (π‘†β€˜π΄) β‰  𝑍) β†’ ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)) = (𝐴 βˆ’ 𝐡))
213124, 212pm2.61dane 3030 1 (πœ‘ β†’ ((π‘€β€˜π΄) βˆ’ (π‘€β€˜π΅)) = (𝐴 βˆ’ 𝐡))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2941   class class class wbr 5149  ran crn 5678  β€˜cfv 6544  (class class class)co 7409  2c2 12267  βŸ¨β€œcs3 14793  Basecbs 17144  distcds 17206  TarskiGcstrkg 27678  DimTarskiGβ‰₯cstrkgld 27682  Itvcitv 27684  LineGclng 27685  pInvGcmir 27903  βˆŸGcrag 27944  βŸ‚Gcperpg 27946  midGcmid 28023  lInvGclmi 28024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-hash 14291  df-word 14465  df-concat 14521  df-s1 14546  df-s2 14799  df-s3 14800  df-trkgc 27699  df-trkgb 27700  df-trkgcb 27701  df-trkgld 27703  df-trkg 27704  df-cgrg 27762  df-leg 27834  df-mir 27904  df-rag 27945  df-perpg 27947  df-mid 28025  df-lmi 28026
This theorem is referenced by:  lmiiso  28048
  Copyright terms: Public domain W3C validator