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 28822

Description: Lemma for lmiiso 28823. (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 28812	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃)
13	1, 2, 3, 4, 7, 8, 12	midcl 28803	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
14		lmiiso.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
15	1, 2, 3, 4, 7, 9, 10, 11, 14	lmicl 28812	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃)
16	1, 2, 3, 4, 7, 14, 15	midcl 28803	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
17	1, 2, 3, 4, 7, 13, 16	midcl 28803	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ 𝑃)
18	6, 17	eqeltrid 2848	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝑃)
20		eqid 2740	. . . . . . . . . 10 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
21		lmiisolem.s	. . . . . . . . . 10 ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍)
22	1, 2, 3, 10, 20, 4, 18, 21, 8	mircl 28687	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐴) ∈ 𝑃)
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) ∈ 𝑃)
24	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝑃)
25	1, 2, 3, 10, 20, 5, 19, 21, 24	mircgr 28683	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
26		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) = 𝑍)
27	26	eqcomd 2746	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = (𝑆‘𝐴))
28	1, 2, 3, 5, 19, 23, 19, 24, 25, 27	tgcgreq 28508	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = 𝐴)
29		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
30	29	oveq2d 7464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))))
31	6, 30	eqtr4id 2799	. . . . . . . . . . 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 28807	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
36	31, 35	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
37		eqidd 2741	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐴))
38	1, 2, 3, 4, 7, 9, 10, 11, 8, 12	islmib 28813	. . . . . . . . . . . . 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 2844	. . . . . . . . 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 28805	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
49	6, 48	eqeltrid 2848	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
50	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
51	1, 3, 10, 43, 44, 45, 46, 47, 50	btwnlng1 28645	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
52	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 ∈ ran 𝐿)
53	40	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
54		eqidd 2741	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐵))
55	1, 2, 3, 4, 7, 9, 10, 11, 14, 15	islmib 28813	. . . . . . . . . . . . . 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 28662	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
60	51, 59	eleqtrrd 2847	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷)
61	42, 60	pm2.61dane 3035	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ 𝐷)
62	61	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝐷)
63	28, 62	eqeltrrd 2845	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝐷)
64	1, 2, 3, 4, 7, 9, 10, 11, 8	lmiinv 28818	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷))
65	64	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐷) → (𝑀‘𝐴) = 𝐴)
66	63, 65	syldan 590	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝐴)
67	66, 28	eqtr4d 2783	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝑍)
68	67	oveq1d 7463	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝑍 − (𝑀‘𝐵)))
69		eqidd 2741	. . . . . . . . 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 28805	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
74	73	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
75		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝑀‘𝐵))
76	75	oveq2d 7464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀‘𝐵)))
77	74, 76	eleqtrrd 2847	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼𝐵))
78	1, 2, 3, 70, 71, 72, 77	axtgbtwnid 28492	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
79		eqidd 2741	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = 𝐵)
80	69, 78, 79	s3eqd 14913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ = ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩)
81	1, 2, 3, 10, 20, 4, 18, 14, 14	ragtrivb 28728	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
83	80, 82	eqeltrrd 2845	. . . . . . 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 2947	. . . . . . . . . 10 ⊢ (𝐵 ≠ (𝑀‘𝐵) ↔ ¬ 𝐵 = (𝑀‘𝐵))
89	56	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵)))
90	89	orcomd 870	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 = (𝑀‘𝐵) ∨ 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵))))
91	90	orcanai 1003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)))
92	88, 91	sylan2b 593	. . . . . . . . 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 28806	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − 𝐵) = (𝐵 − (𝑀‘𝐵)))
102	101	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − (𝑀‘𝐵)) = (𝐵 − 𝐵))
103	1, 2, 3, 96, 97, 98, 97, 102	axtgcgrid 28489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 = (𝑀‘𝐵))
104	103	ex 412	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵 → 𝐵 = (𝑀‘𝐵)))
105	104	necon3d 2967	. . . . . . . . . . . 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 28645	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐿(𝑀‘𝐵)))
109	1, 3, 10, 84, 87, 93, 94, 95, 106, 108	tglineelsb2 28658	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
110	1, 3, 10, 84, 95, 87, 106	tglinecom 28661	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
111	109, 110	eqtr4d 2783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
112	92, 111	breqtrd 5192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
113	1, 2, 3, 10, 84, 85, 86, 87, 112	perpdrag 28754	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
114	83, 113	pm2.61dane 3035	. . . . . 6 ⊢ (𝜑 → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
115	1, 2, 3, 10, 20, 4, 18, 16, 14	israg 28723	. . . . . 6 ⊢ (𝜑 → (⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))))
116	114, 115	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
117		eqidd 2741	. . . . . . 7 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
118	1, 2, 3, 4, 7, 14, 15, 20, 16	ismidb 28804	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
119	117, 118	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))
120	119	oveq2d 7464	. . . . 5 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐵)) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
121	116, 120	eqtr4d 2783	. . . 4 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
122	121	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
123	28	oveq1d 7463	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝐴 − 𝐵))
124	68, 122, 123	3eqtr2d 2786	. 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 28687	. . . . 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 28684	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘𝐴)𝐼𝐴))
136	1, 2, 3, 10, 20, 125, 127, 21, 131	mirbtwn 28684	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘(𝑀‘𝐴))𝐼(𝑀‘𝐴)))
137		eqidd 2741	. . . . . . . . . . . 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 28805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
142	141	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
143		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝑀‘𝐴))
144	143	oveq2d 7464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀‘𝐴)))
145	142, 144	eleqtrrd 2847	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼𝐴))
146	1, 2, 3, 138, 139, 140, 145	axtgbtwnid 28492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
147		eqidd 2741	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = 𝐴)
148	137, 146, 147	s3eqd 14913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ = ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩)
149	1, 2, 3, 10, 20, 4, 18, 8, 8	ragtrivb 28728	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
150	149	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
151	148, 150	eqeltrrd 2845	. . . . . . . . . 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 2947	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ (𝑀‘𝐴) ↔ ¬ 𝐴 = (𝑀‘𝐴))
157	39	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴)))
158	157	orcomd 870	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = (𝑀‘𝐴) ∨ 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴))))
159	158	orcanai 1003	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐴 = (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)))
160	156, 159	sylan2b 593	. . . . . . . . . . . 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 28806	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − 𝐴) = (𝐴 − (𝑀‘𝐴)))
170	169	eqcomd 2746	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − (𝑀‘𝐴)) = (𝐴 − 𝐴))
171	1, 2, 3, 164, 165, 166, 165, 170	axtgcgrid 28489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 = (𝑀‘𝐴))
172	171	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴 → 𝐴 = (𝑀‘𝐴)))
173	172	necon3d 2967	. . . . . . . . . . . . . . 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 28645	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐿(𝑀‘𝐴)))
177	1, 3, 10, 152, 155, 161, 162, 163, 174, 176	tglineelsb2 28658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
178	1, 3, 10, 152, 163, 155, 174	tglinecom 28661	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
179	177, 178	eqtr4d 2783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
180	160, 179	breqtrd 5192	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
181	1, 2, 3, 10, 152, 153, 154, 155, 180	perpdrag 28754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
182	151, 181	pm2.61dane 3035	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
183	1, 2, 3, 10, 20, 4, 18, 13, 8	israg 28723	. . . . . . . . 9 ⊢ (𝜑 → (⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))))
184	182, 183	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
185		eqidd 2741	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
186	1, 2, 3, 4, 7, 8, 12, 20, 13	ismidb 28804	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴))))
187	185, 186	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))
188	187	oveq2d 7464	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐴)) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
189	184, 188	eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
190	1, 2, 3, 10, 20, 4, 18, 21, 8	mircgr 28683	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
191	1, 2, 3, 10, 20, 4, 18, 21, 12	mircgr 28683	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘(𝑀‘𝐴))) = (𝑍 − (𝑀‘𝐴)))
192	189, 190, 191	3eqtr4d 2790	. . . . . 6 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
193	192	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
194	1, 2, 3, 125, 127, 126, 127, 130, 193	tgcgrcomlr 28506	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝑍) = ((𝑆‘(𝑀‘𝐴)) − 𝑍))
195	189	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
196	21	fveq1i 6921	. . . . . . . . . 10 ⊢ (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))
197	1, 2, 3, 4, 7, 8, 12, 21, 18	mirmid 28809	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
198	6	eqcomi 2749	. . . . . . . . . . 11 ⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍
199	1, 2, 3, 4, 7, 13, 16, 20, 18	ismidb 28804	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍))
200	198, 199	mpbiri 258	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
201	196, 197, 200	3eqtr4a 2806	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
202	1, 2, 3, 4, 7, 22, 129, 20, 16	ismidb 28804	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)) ↔ ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
203	201, 202	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)))
204	119, 203	oveq12d 7466	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))) = ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))))
205		eqid 2740	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵))) = ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))
206	1, 2, 3, 10, 20, 4, 16, 205, 14, 22	miriso 28696	. . . . . . 7 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))) = (𝐵 − (𝑆‘𝐴)))
207	204, 206	eqtr2d 2781	. . . . . 6 ⊢ (𝜑 → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
208	207	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
209	1, 2, 3, 125, 132, 126, 133, 130, 208	tgcgrcomlr 28506	. . . 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 28491	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐴 − 𝐵) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
212	211	eqcomd 2746	. 2 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))
213	124, 212	pm2.61dane 3035	1 ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 class class class wbr 5166 ran crn 5701 ‘cfv 6573 (class class class)co 7448 2c2 12348 ⟨“cs3 14891 Basecbs 17258 distcds 17320 TarskiGcstrkg 28453 Dim_TarskiG≥cstrkgld 28457 Itvcitv 28459 LineGclng 28460 pInvGcmir 28678 ∟Gcrag 28719 ⟂Gcperpg 28721 midGcmid 28798 lInvGclmi 28799

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-oadd 8526 df-er 8763 df-map 8886 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-xnn0 12626 df-z 12640 df-uz 12904 df-fz 13568 df-fzo 13712 df-hash 14380 df-word 14563 df-concat 14619 df-s1 14644 df-s2 14897 df-s3 14898 df-trkgc 28474 df-trkgb 28475 df-trkgcb 28476 df-trkgld 28478 df-trkg 28479 df-cgrg 28537 df-leg 28609 df-mir 28679 df-rag 28720 df-perpg 28722 df-mid 28800 df-lmi 28801

This theorem is referenced by: lmiiso 28823

W3C validator