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

Theorem lmiisolem 25908
 Description: Lemma for lmiiso 25909. (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 472 . . . . . . . 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 25898 . . . . . . . . . . . 12 (𝜑 → (𝑀𝐴) ∈ 𝑃)
131, 2, 3, 4, 7, 8, 12midcl 25889 . . . . . . . . . . 11 (𝜑 → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝑃)
14 lmiiso.2 . . . . . . . . . . . 12 (𝜑𝐵𝑃)
151, 2, 3, 4, 7, 9, 10, 11, 14lmicl 25898 . . . . . . . . . . . 12 (𝜑 → (𝑀𝐵) ∈ 𝑃)
161, 2, 3, 4, 7, 14, 15midcl 25889 . . . . . . . . . . 11 (𝜑 → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝑃)
171, 2, 3, 4, 7, 13, 16midcl 25889 . . . . . . . . . 10 (𝜑 → ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀𝐵))) ∈ 𝑃)
186, 17syl5eqel 2843 . . . . . . . . 9 (𝜑𝑍𝑃)
1918adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝑍𝑃)
20 eqid 2760 . . . . . . . . . 10 (pInvG‘𝐺) = (pInvG‘𝐺)
21 lmiisolem.s . . . . . . . . . 10 𝑆 = ((pInvG‘𝐺)‘𝑍)
221, 2, 3, 10, 20, 4, 18, 21, 8mircl 25776 . . . . . . . . 9 (𝜑 → (𝑆𝐴) ∈ 𝑃)
2322adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑆𝐴) ∈ 𝑃)
248adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝐴𝑃)
251, 2, 3, 10, 20, 5, 19, 21, 24mircgr 25772 . . . . . . . 8 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑍 (𝑆𝐴)) = (𝑍 𝐴))
26 simpr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑆𝐴) = 𝑍)
2726eqcomd 2766 . . . . . . . 8 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝑍 = (𝑆𝐴))
281, 2, 3, 5, 19, 23, 19, 24, 25, 27tgcgreq 25597 . . . . . . 7 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝑍 = 𝐴)
29 simpr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵)))
3029oveq2d 6830 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀𝐴))) = ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀𝐵))))
3130, 6syl6reqr 2813 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍 = ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀𝐴))))
324adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝐺 ∈ TarskiG)
337adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝐺DimTarskiG≥2)
3413adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝑃)
351, 2, 3, 32, 33, 34, 34midid 25893 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀𝐴))) = (𝐴(midG‘𝐺)(𝑀𝐴)))
3631, 35eqtrd 2794 . . . . . . . . . 10 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍 = (𝐴(midG‘𝐺)(𝑀𝐴)))
37 eqidd 2761 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝐴) = (𝑀𝐴))
381, 2, 3, 4, 7, 9, 10, 11, 8, 12islmib 25899 . . . . . . . . . . . . 13 (𝜑 → ((𝑀𝐴) = (𝑀𝐴) ↔ ((𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴)) ∨ 𝐴 = (𝑀𝐴)))))
3937, 38mpbid 222 . . . . . . . . . . . 12 (𝜑 → ((𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴)) ∨ 𝐴 = (𝑀𝐴))))
4039simpld 477 . . . . . . . . . . 11 (𝜑 → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷)
4140adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷)
4236, 41eqeltrd 2839 . . . . . . . . 9 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍𝐷)
434adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝐺 ∈ TarskiG)
4413adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝑃)
4516adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝑃)
4618adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍𝑃)
47 simpr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵)))
481, 2, 3, 4, 7, 13, 16midbtwn 25891 . . . . . . . . . . . . 13 (𝜑 → ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀𝐵))) ∈ ((𝐴(midG‘𝐺)(𝑀𝐴))𝐼(𝐵(midG‘𝐺)(𝑀𝐵))))
496, 48syl5eqel 2843 . . . . . . . . . . . 12 (𝜑𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀𝐴))𝐼(𝐵(midG‘𝐺)(𝑀𝐵))))
5049adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀𝐴))𝐼(𝐵(midG‘𝐺)(𝑀𝐵))))
511, 3, 10, 43, 44, 45, 46, 47, 50btwnlng1 25734 . . . . . . . . . 10 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀𝐴))𝐿(𝐵(midG‘𝐺)(𝑀𝐵))))
5211adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝐷 ∈ ran 𝐿)
5340adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷)
54 eqidd 2761 . . . . . . . . . . . . . 14 (𝜑 → (𝑀𝐵) = (𝑀𝐵))
551, 2, 3, 4, 7, 9, 10, 11, 14, 15islmib 25899 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀𝐵) = (𝑀𝐵) ↔ ((𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵)) ∨ 𝐵 = (𝑀𝐵)))))
5654, 55mpbid 222 . . . . . . . . . . . . 13 (𝜑 → ((𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵)) ∨ 𝐵 = (𝑀𝐵))))
5756simpld 477 . . . . . . . . . . . 12 (𝜑 → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝐷)
5857adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝐷)
591, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58tglinethru 25751 . . . . . . . . . 10 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝐷 = ((𝐴(midG‘𝐺)(𝑀𝐴))𝐿(𝐵(midG‘𝐺)(𝑀𝐵))))
6051, 59eleqtrrd 2842 . . . . . . . . 9 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀𝐵))) → 𝑍𝐷)
6142, 60pm2.61dane 3019 . . . . . . . 8 (𝜑𝑍𝐷)
6261adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝑍𝐷)
6328, 62eqeltrrd 2840 . . . . . 6 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → 𝐴𝐷)
641, 2, 3, 4, 7, 9, 10, 11, 8lmiinv 25904 . . . . . . 7 (𝜑 → ((𝑀𝐴) = 𝐴𝐴𝐷))
6564biimpar 503 . . . . . 6 ((𝜑𝐴𝐷) → (𝑀𝐴) = 𝐴)
6663, 65syldan 488 . . . . 5 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑀𝐴) = 𝐴)
6766, 28eqtr4d 2797 . . . 4 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑀𝐴) = 𝑍)
6867oveq1d 6829 . . 3 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → ((𝑀𝐴) (𝑀𝐵)) = (𝑍 (𝑀𝐵)))
69 eqidd 2761 . . . . . . . . 9 ((𝜑𝐵 = (𝑀𝐵)) → 𝑍 = 𝑍)
704adantr 472 . . . . . . . . . 10 ((𝜑𝐵 = (𝑀𝐵)) → 𝐺 ∈ TarskiG)
7114adantr 472 . . . . . . . . . 10 ((𝜑𝐵 = (𝑀𝐵)) → 𝐵𝑃)
7216adantr 472 . . . . . . . . . 10 ((𝜑𝐵 = (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝑃)
731, 2, 3, 4, 7, 14, 15midbtwn 25891 . . . . . . . . . . . 12 (𝜑 → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ (𝐵𝐼(𝑀𝐵)))
7473adantr 472 . . . . . . . . . . 11 ((𝜑𝐵 = (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ (𝐵𝐼(𝑀𝐵)))
75 simpr 479 . . . . . . . . . . . 12 ((𝜑𝐵 = (𝑀𝐵)) → 𝐵 = (𝑀𝐵))
7675oveq2d 6830 . . . . . . . . . . 11 ((𝜑𝐵 = (𝑀𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀𝐵)))
7774, 76eleqtrrd 2842 . . . . . . . . . 10 ((𝜑𝐵 = (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ (𝐵𝐼𝐵))
781, 2, 3, 70, 71, 72, 77axtgbtwnid 25585 . . . . . . . . 9 ((𝜑𝐵 = (𝑀𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀𝐵)))
79 eqidd 2761 . . . . . . . . 9 ((𝜑𝐵 = (𝑀𝐵)) → 𝐵 = 𝐵)
8069, 78, 79s3eqd 13829 . . . . . . . 8 ((𝜑𝐵 = (𝑀𝐵)) → ⟨“𝑍𝐵𝐵”⟩ = ⟨“𝑍(𝐵(midG‘𝐺)(𝑀𝐵))𝐵”⟩)
811, 2, 3, 10, 20, 4, 18, 14, 14ragtrivb 25817 . . . . . . . . 9 (𝜑 → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
8281adantr 472 . . . . . . . 8 ((𝜑𝐵 = (𝑀𝐵)) → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
8380, 82eqeltrrd 2840 . . . . . . 7 ((𝜑𝐵 = (𝑀𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
844adantr 472 . . . . . . . 8 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝐺 ∈ TarskiG)
8561adantr 472 . . . . . . . 8 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝑍𝐷)
8657adantr 472 . . . . . . . 8 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝐷)
8714adantr 472 . . . . . . . 8 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝐵𝑃)
88 df-ne 2933 . . . . . . . . . 10 (𝐵 ≠ (𝑀𝐵) ↔ ¬ 𝐵 = (𝑀𝐵))
8956simprd 482 . . . . . . . . . . . 12 (𝜑 → (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵)) ∨ 𝐵 = (𝑀𝐵)))
9089orcomd 402 . . . . . . . . . . 11 (𝜑 → (𝐵 = (𝑀𝐵) ∨ 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵))))
9190orcanai 990 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵 = (𝑀𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵)))
9288, 91sylan2b 493 . . . . . . . . 9 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀𝐵)))
9315adantr 472 . . . . . . . . . . 11 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝑀𝐵) ∈ 𝑃)
94 simpr 479 . . . . . . . . . . 11 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝐵 ≠ (𝑀𝐵))
9516adantr 472 . . . . . . . . . . 11 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ 𝑃)
964adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → 𝐺 ∈ TarskiG)
9714adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → 𝐵𝑃)
9815adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → (𝑀𝐵) ∈ 𝑃)
997adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → 𝐺DimTarskiG≥2)
100 simpr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵)
1011, 2, 3, 96, 99, 97, 98, 100midcgr 25892 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → (𝐵 𝐵) = (𝐵 (𝑀𝐵)))
102101eqcomd 2766 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → (𝐵 (𝑀𝐵)) = (𝐵 𝐵))
1031, 2, 3, 96, 97, 98, 97, 102axtgcgrid 25582 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵) → 𝐵 = (𝑀𝐵))
104103ex 449 . . . . . . . . . . . . 13 (𝜑 → ((𝐵(midG‘𝐺)(𝑀𝐵)) = 𝐵𝐵 = (𝑀𝐵)))
105104necon3d 2953 . . . . . . . . . . . 12 (𝜑 → (𝐵 ≠ (𝑀𝐵) → (𝐵(midG‘𝐺)(𝑀𝐵)) ≠ 𝐵))
106105imp 444 . . . . . . . . . . 11 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ≠ 𝐵)
10773adantr 472 . . . . . . . . . . . 12 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ (𝐵𝐼(𝑀𝐵)))
1081, 3, 10, 84, 87, 93, 95, 94, 107btwnlng1 25734 . . . . . . . . . . 11 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵(midG‘𝐺)(𝑀𝐵)) ∈ (𝐵𝐿(𝑀𝐵)))
1091, 3, 10, 84, 87, 93, 94, 95, 106, 108tglineelsb2 25747 . . . . . . . . . 10 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵𝐿(𝑀𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀𝐵))))
1101, 3, 10, 84, 95, 87, 106tglinecom 25750 . . . . . . . . . 10 ((𝜑𝐵 ≠ (𝑀𝐵)) → ((𝐵(midG‘𝐺)(𝑀𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀𝐵))))
111109, 110eqtr4d 2797 . . . . . . . . 9 ((𝜑𝐵 ≠ (𝑀𝐵)) → (𝐵𝐿(𝑀𝐵)) = ((𝐵(midG‘𝐺)(𝑀𝐵))𝐿𝐵))
11292, 111breqtrd 4830 . . . . . . . 8 ((𝜑𝐵 ≠ (𝑀𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀𝐵))𝐿𝐵))
1131, 2, 3, 10, 84, 85, 86, 87, 112perpdrag 25840 . . . . . . 7 ((𝜑𝐵 ≠ (𝑀𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
11483, 113pm2.61dane 3019 . . . . . 6 (𝜑 → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
1151, 2, 3, 10, 20, 4, 18, 16, 14israg 25812 . . . . . 6 (𝜑 → (⟨“𝑍(𝐵(midG‘𝐺)(𝑀𝐵))𝐵”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 𝐵) = (𝑍 (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵))))
116114, 115mpbid 222 . . . . 5 (𝜑 → (𝑍 𝐵) = (𝑍 (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵)))
117 eqidd 2761 . . . . . . 7 (𝜑 → (𝐵(midG‘𝐺)(𝑀𝐵)) = (𝐵(midG‘𝐺)(𝑀𝐵)))
1181, 2, 3, 4, 7, 14, 15, 20, 16ismidb 25890 . . . . . . 7 (𝜑 → ((𝑀𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀𝐵)) = (𝐵(midG‘𝐺)(𝑀𝐵))))
119117, 118mpbird 247 . . . . . 6 (𝜑 → (𝑀𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵))
120119oveq2d 6830 . . . . 5 (𝜑 → (𝑍 (𝑀𝐵)) = (𝑍 (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵)))
121116, 120eqtr4d 2797 . . . 4 (𝜑 → (𝑍 𝐵) = (𝑍 (𝑀𝐵)))
122121adantr 472 . . 3 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑍 𝐵) = (𝑍 (𝑀𝐵)))
12328oveq1d 6829 . . 3 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → (𝑍 𝐵) = (𝐴 𝐵))
12468, 122, 1233eqtr2d 2800 . 2 ((𝜑 ∧ (𝑆𝐴) = 𝑍) → ((𝑀𝐴) (𝑀𝐵)) = (𝐴 𝐵))
1254adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝐺 ∈ TarskiG)
12622adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑆𝐴) ∈ 𝑃)
12718adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝑍𝑃)
1288adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝐴𝑃)
1291, 2, 3, 10, 20, 4, 18, 21, 12mircl 25776 . . . . 5 (𝜑 → (𝑆‘(𝑀𝐴)) ∈ 𝑃)
130129adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑆‘(𝑀𝐴)) ∈ 𝑃)
13112adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑀𝐴) ∈ 𝑃)
13214adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝐵𝑃)
13315adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑀𝐵) ∈ 𝑃)
134 simpr 479 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑆𝐴) ≠ 𝑍)
1351, 2, 3, 10, 20, 125, 127, 21, 128mirbtwn 25773 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆𝐴)𝐼𝐴))
1361, 2, 3, 10, 20, 125, 127, 21, 131mirbtwn 25773 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘(𝑀𝐴))𝐼(𝑀𝐴)))
137 eqidd 2761 . . . . . . . . . . . 12 ((𝜑𝐴 = (𝑀𝐴)) → 𝑍 = 𝑍)
1384adantr 472 . . . . . . . . . . . . 13 ((𝜑𝐴 = (𝑀𝐴)) → 𝐺 ∈ TarskiG)
1398adantr 472 . . . . . . . . . . . . 13 ((𝜑𝐴 = (𝑀𝐴)) → 𝐴𝑃)
14013adantr 472 . . . . . . . . . . . . 13 ((𝜑𝐴 = (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝑃)
1411, 2, 3, 4, 7, 8, 12midbtwn 25891 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ (𝐴𝐼(𝑀𝐴)))
142141adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝐴 = (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ (𝐴𝐼(𝑀𝐴)))
143 simpr 479 . . . . . . . . . . . . . . 15 ((𝜑𝐴 = (𝑀𝐴)) → 𝐴 = (𝑀𝐴))
144143oveq2d 6830 . . . . . . . . . . . . . 14 ((𝜑𝐴 = (𝑀𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀𝐴)))
145142, 144eleqtrrd 2842 . . . . . . . . . . . . 13 ((𝜑𝐴 = (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ (𝐴𝐼𝐴))
1461, 2, 3, 138, 139, 140, 145axtgbtwnid 25585 . . . . . . . . . . . 12 ((𝜑𝐴 = (𝑀𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀𝐴)))
147 eqidd 2761 . . . . . . . . . . . 12 ((𝜑𝐴 = (𝑀𝐴)) → 𝐴 = 𝐴)
148137, 146, 147s3eqd 13829 . . . . . . . . . . 11 ((𝜑𝐴 = (𝑀𝐴)) → ⟨“𝑍𝐴𝐴”⟩ = ⟨“𝑍(𝐴(midG‘𝐺)(𝑀𝐴))𝐴”⟩)
1491, 2, 3, 10, 20, 4, 18, 8, 8ragtrivb 25817 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
150149adantr 472 . . . . . . . . . . 11 ((𝜑𝐴 = (𝑀𝐴)) → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
151148, 150eqeltrrd 2840 . . . . . . . . . 10 ((𝜑𝐴 = (𝑀𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
1524adantr 472 . . . . . . . . . . 11 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝐺 ∈ TarskiG)
15361adantr 472 . . . . . . . . . . 11 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝑍𝐷)
15440adantr 472 . . . . . . . . . . 11 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝐷)
1558adantr 472 . . . . . . . . . . 11 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝐴𝑃)
156 df-ne 2933 . . . . . . . . . . . . 13 (𝐴 ≠ (𝑀𝐴) ↔ ¬ 𝐴 = (𝑀𝐴))
15739simprd 482 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴)) ∨ 𝐴 = (𝑀𝐴)))
158157orcomd 402 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = (𝑀𝐴) ∨ 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴))))
159158orcanai 990 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐴 = (𝑀𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴)))
160156, 159sylan2b 493 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀𝐴)))
16112adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝑀𝐴) ∈ 𝑃)
162 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝐴 ≠ (𝑀𝐴))
16313adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ 𝑃)
1644adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → 𝐺 ∈ TarskiG)
1658adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → 𝐴𝑃)
16612adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → (𝑀𝐴) ∈ 𝑃)
1677adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → 𝐺DimTarskiG≥2)
168 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴)
1691, 2, 3, 164, 167, 165, 166, 168midcgr 25892 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → (𝐴 𝐴) = (𝐴 (𝑀𝐴)))
170169eqcomd 2766 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → (𝐴 (𝑀𝐴)) = (𝐴 𝐴))
1711, 2, 3, 164, 165, 166, 165, 170axtgcgrid 25582 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴) → 𝐴 = (𝑀𝐴))
172171ex 449 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴(midG‘𝐺)(𝑀𝐴)) = 𝐴𝐴 = (𝑀𝐴)))
173172necon3d 2953 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 ≠ (𝑀𝐴) → (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ 𝐴))
174173imp 444 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ≠ 𝐴)
175141adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ (𝐴𝐼(𝑀𝐴)))
1761, 3, 10, 152, 155, 161, 163, 162, 175btwnlng1 25734 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴(midG‘𝐺)(𝑀𝐴)) ∈ (𝐴𝐿(𝑀𝐴)))
1771, 3, 10, 152, 155, 161, 162, 163, 174, 176tglineelsb2 25747 . . . . . . . . . . . . 13 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴𝐿(𝑀𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀𝐴))))
1781, 3, 10, 152, 163, 155, 174tglinecom 25750 . . . . . . . . . . . . 13 ((𝜑𝐴 ≠ (𝑀𝐴)) → ((𝐴(midG‘𝐺)(𝑀𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀𝐴))))
179177, 178eqtr4d 2797 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ (𝑀𝐴)) → (𝐴𝐿(𝑀𝐴)) = ((𝐴(midG‘𝐺)(𝑀𝐴))𝐿𝐴))
180160, 179breqtrd 4830 . . . . . . . . . . 11 ((𝜑𝐴 ≠ (𝑀𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀𝐴))𝐿𝐴))
1811, 2, 3, 10, 152, 153, 154, 155, 180perpdrag 25840 . . . . . . . . . 10 ((𝜑𝐴 ≠ (𝑀𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
182151, 181pm2.61dane 3019 . . . . . . . . 9 (𝜑 → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
1831, 2, 3, 10, 20, 4, 18, 13, 8israg 25812 . . . . . . . . 9 (𝜑 → (⟨“𝑍(𝐴(midG‘𝐺)(𝑀𝐴))𝐴”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 𝐴) = (𝑍 (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀𝐴)))‘𝐴))))
184182, 183mpbid 222 . . . . . . . 8 (𝜑 → (𝑍 𝐴) = (𝑍 (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀𝐴)))‘𝐴)))
185 eqidd 2761 . . . . . . . . . 10 (𝜑 → (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐴(midG‘𝐺)(𝑀𝐴)))
1861, 2, 3, 4, 7, 8, 12, 20, 13ismidb 25890 . . . . . . . . . 10 (𝜑 → ((𝑀𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀𝐴)) = (𝐴(midG‘𝐺)(𝑀𝐴))))
187185, 186mpbird 247 . . . . . . . . 9 (𝜑 → (𝑀𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀𝐴)))‘𝐴))
188187oveq2d 6830 . . . . . . . 8 (𝜑 → (𝑍 (𝑀𝐴)) = (𝑍 (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀𝐴)))‘𝐴)))
189184, 188eqtr4d 2797 . . . . . . 7 (𝜑 → (𝑍 𝐴) = (𝑍 (𝑀𝐴)))
1901, 2, 3, 10, 20, 4, 18, 21, 8mircgr 25772 . . . . . . 7 (𝜑 → (𝑍 (𝑆𝐴)) = (𝑍 𝐴))
1911, 2, 3, 10, 20, 4, 18, 21, 12mircgr 25772 . . . . . . 7 (𝜑 → (𝑍 (𝑆‘(𝑀𝐴))) = (𝑍 (𝑀𝐴)))
192189, 190, 1913eqtr4d 2804 . . . . . 6 (𝜑 → (𝑍 (𝑆𝐴)) = (𝑍 (𝑆‘(𝑀𝐴))))
193192adantr 472 . . . . 5 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑍 (𝑆𝐴)) = (𝑍 (𝑆‘(𝑀𝐴))))
1941, 2, 3, 125, 127, 126, 127, 130, 193tgcgrcomlr 25595 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → ((𝑆𝐴) 𝑍) = ((𝑆‘(𝑀𝐴)) 𝑍))
195189adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑍 𝐴) = (𝑍 (𝑀𝐴)))
19621fveq1i 6354 . . . . . . . . . 10 (𝑆‘(𝐴(midG‘𝐺)(𝑀𝐴))) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀𝐴)))
1971, 2, 3, 4, 7, 8, 12, 21, 18mirmid 25895 . . . . . . . . . 10 (𝜑 → ((𝑆𝐴)(midG‘𝐺)(𝑆‘(𝑀𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀𝐴))))
1986eqcomi 2769 . . . . . . . . . . 11 ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀𝐵))) = 𝑍
1991, 2, 3, 4, 7, 13, 16, 20, 18ismidb 25890 . . . . . . . . . . 11 (𝜑 → ((𝐵(midG‘𝐺)(𝑀𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀𝐴))) ↔ ((𝐴(midG‘𝐺)(𝑀𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀𝐵))) = 𝑍))
200198, 199mpbiri 248 . . . . . . . . . 10 (𝜑 → (𝐵(midG‘𝐺)(𝑀𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀𝐴))))
201196, 197, 2003eqtr4a 2820 . . . . . . . . 9 (𝜑 → ((𝑆𝐴)(midG‘𝐺)(𝑆‘(𝑀𝐴))) = (𝐵(midG‘𝐺)(𝑀𝐵)))
2021, 2, 3, 4, 7, 22, 129, 20, 16ismidb 25890 . . . . . . . . 9 (𝜑 → ((𝑆‘(𝑀𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘(𝑆𝐴)) ↔ ((𝑆𝐴)(midG‘𝐺)(𝑆‘(𝑀𝐴))) = (𝐵(midG‘𝐺)(𝑀𝐵))))
203201, 202mpbird 247 . . . . . . . 8 (𝜑 → (𝑆‘(𝑀𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘(𝑆𝐴)))
204119, 203oveq12d 6832 . . . . . . 7 (𝜑 → ((𝑀𝐵) (𝑆‘(𝑀𝐴))) = ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵) (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘(𝑆𝐴))))
205 eqid 2760 . . . . . . . 8 ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵))) = ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))
2061, 2, 3, 10, 20, 4, 16, 205, 14, 22miriso 25785 . . . . . . 7 (𝜑 → ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘𝐵) (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀𝐵)))‘(𝑆𝐴))) = (𝐵 (𝑆𝐴)))
207204, 206eqtr2d 2795 . . . . . 6 (𝜑 → (𝐵 (𝑆𝐴)) = ((𝑀𝐵) (𝑆‘(𝑀𝐴))))
208207adantr 472 . . . . 5 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝐵 (𝑆𝐴)) = ((𝑀𝐵) (𝑆‘(𝑀𝐴))))
2091, 2, 3, 125, 132, 126, 133, 130, 208tgcgrcomlr 25595 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → ((𝑆𝐴) 𝐵) = ((𝑆‘(𝑀𝐴)) (𝑀𝐵)))
210121adantr 472 . . . 4 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝑍 𝐵) = (𝑍 (𝑀𝐵)))
2111, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210axtg5seg 25584 . . 3 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → (𝐴 𝐵) = ((𝑀𝐴) (𝑀𝐵)))
212211eqcomd 2766 . 2 ((𝜑 ∧ (𝑆𝐴) ≠ 𝑍) → ((𝑀𝐴) (𝑀𝐵)) = (𝐴 𝐵))
213124, 212pm2.61dane 3019 1 (𝜑 → ((𝑀𝐴) (𝑀𝐵)) = (𝐴 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932   class class class wbr 4804  ran crn 5267  ‘cfv 6049  (class class class)co 6814  2c2 11282  ⟨“cs3 13807  Basecbs 16079  distcds 16172  TarskiGcstrkg 25549  DimTarskiG≥cstrkgld 25553  Itvcitv 25555  LineGclng 25556  pInvGcmir 25767  ∟Gcrag 25808  ⟂Gcperpg 25810  midGcmid 25884  lInvGclmi 25885 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233  df-2 11291  df-3 11292  df-n0 11505  df-xnn0 11576  df-z 11590  df-uz 11900  df-fz 12540  df-fzo 12680  df-hash 13332  df-word 13505  df-concat 13507  df-s1 13508  df-s2 13813  df-s3 13814  df-trkgc 25567  df-trkgb 25568  df-trkgcb 25569  df-trkgld 25571  df-trkg 25572  df-cgrg 25626  df-leg 25698  df-mir 25768  df-rag 25809  df-perpg 25811  df-mid 25886  df-lmi 25887 This theorem is referenced by:  lmiiso  25909
 Copyright terms: Public domain W3C validator