lmiisolem - Metamath Proof Explorer

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

Theorem lmiisolem 28864

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

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 class class class wbr 5085 ran crn 5632 ‘cfv 6498 (class class class)co 7367 2c2 12236 ⟨“cs3 14804 Basecbs 17179 distcds 17229 TarskiGcstrkg 28495 Dim_TarskiG≥cstrkgld 28499 Itvcitv 28501 LineGclng 28502 pInvGcmir 28720 ∟Gcrag 28761 ⟂Gcperpg 28763 midGcmid 28840 lInvGclmi 28841

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-oadd 8409 df-er 8643 df-map 8775 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-dju 9825 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-xnn0 12511 df-z 12525 df-uz 12789 df-fz 13462 df-fzo 13609 df-hash 14293 df-word 14476 df-concat 14533 df-s1 14559 df-s2 14810 df-s3 14811 df-trkgc 28516 df-trkgb 28517 df-trkgcb 28518 df-trkgld 28520 df-trkg 28521 df-cgrg 28579 df-leg 28651 df-mir 28721 df-rag 28762 df-perpg 28764 df-mid 28842 df-lmi 28843

This theorem is referenced by: lmiiso 28865

W3C validator