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 28741

Description: Lemma for lmiiso 28742. (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 28731	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃)
13	1, 2, 3, 4, 7, 8, 12	midcl 28722	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
14		lmiiso.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
15	1, 2, 3, 4, 7, 9, 10, 11, 14	lmicl 28731	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃)
16	1, 2, 3, 4, 7, 14, 15	midcl 28722	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
17	1, 2, 3, 4, 7, 13, 16	midcl 28722	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ 𝑃)
18	6, 17	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝑃)
20		eqid 2729	. . . . . . . . . 10 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
21		lmiisolem.s	. . . . . . . . . 10 ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍)
22	1, 2, 3, 10, 20, 4, 18, 21, 8	mircl 28606	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐴) ∈ 𝑃)
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) ∈ 𝑃)
24	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝑃)
25	1, 2, 3, 10, 20, 5, 19, 21, 24	mircgr 28602	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
26		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) = 𝑍)
27	26	eqcomd 2735	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = (𝑆‘𝐴))
28	1, 2, 3, 5, 19, 23, 19, 24, 25, 27	tgcgreq 28427	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = 𝐴)
29		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
30	29	oveq2d 7365	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))))
31	6, 30	eqtr4id 2783	. . . . . . . . . . 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 28726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
36	31, 35	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
37		eqidd 2730	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐴))
38	1, 2, 3, 4, 7, 9, 10, 11, 8, 12	islmib 28732	. . . . . . . . . . . . 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 2828	. . . . . . . . 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 28724	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
49	6, 48	eqeltrid 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
50	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
51	1, 3, 10, 43, 44, 45, 46, 47, 50	btwnlng1 28564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
52	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 ∈ ran 𝐿)
53	40	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
54		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐵))
55	1, 2, 3, 4, 7, 9, 10, 11, 14, 15	islmib 28732	. . . . . . . . . . . . . 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 28581	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
60	51, 59	eleqtrrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷)
61	42, 60	pm2.61dane 3012	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ 𝐷)
62	61	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝐷)
63	28, 62	eqeltrrd 2829	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝐷)
64	1, 2, 3, 4, 7, 9, 10, 11, 8	lmiinv 28737	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷))
65	64	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐷) → (𝑀‘𝐴) = 𝐴)
66	63, 65	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝐴)
67	66, 28	eqtr4d 2767	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝑍)
68	67	oveq1d 7364	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝑍 − (𝑀‘𝐵)))
69		eqidd 2730	. . . . . . . . 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 28724	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
74	73	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
75		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝑀‘𝐵))
76	75	oveq2d 7365	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀‘𝐵)))
77	74, 76	eleqtrrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼𝐵))
78	1, 2, 3, 70, 71, 72, 77	axtgbtwnid 28411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
79		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = 𝐵)
80	69, 78, 79	s3eqd 14771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ = ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩)
81	1, 2, 3, 10, 20, 4, 18, 14, 14	ragtrivb 28647	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
83	80, 82	eqeltrrd 2829	. . . . . . 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 2926	. . . . . . . . . 10 ⊢ (𝐵 ≠ (𝑀‘𝐵) ↔ ¬ 𝐵 = (𝑀‘𝐵))
89	56	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵)))
90	89	orcomd 871	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 = (𝑀‘𝐵) ∨ 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵))))
91	90	orcanai 1004	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)))
92	88, 91	sylan2b 594	. . . . . . . . 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 28725	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − 𝐵) = (𝐵 − (𝑀‘𝐵)))
102	101	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − (𝑀‘𝐵)) = (𝐵 − 𝐵))
103	1, 2, 3, 96, 97, 98, 97, 102	axtgcgrid 28408	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 = (𝑀‘𝐵))
104	103	ex 412	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵 → 𝐵 = (𝑀‘𝐵)))
105	104	necon3d 2946	. . . . . . . . . . . 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 28564	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐿(𝑀‘𝐵)))
109	1, 3, 10, 84, 87, 93, 94, 95, 106, 108	tglineelsb2 28577	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
110	1, 3, 10, 84, 95, 87, 106	tglinecom 28580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
111	109, 110	eqtr4d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
112	92, 111	breqtrd 5118	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
113	1, 2, 3, 10, 84, 85, 86, 87, 112	perpdrag 28673	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
114	83, 113	pm2.61dane 3012	. . . . . 6 ⊢ (𝜑 → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
115	1, 2, 3, 10, 20, 4, 18, 16, 14	israg 28642	. . . . . 6 ⊢ (𝜑 → (⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))))
116	114, 115	mpbid 232	. . . . 5 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
117		eqidd 2730	. . . . . . 7 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
118	1, 2, 3, 4, 7, 14, 15, 20, 16	ismidb 28723	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
119	117, 118	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))
120	119	oveq2d 7365	. . . . 5 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐵)) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
121	116, 120	eqtr4d 2767	. . . 4 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
122	121	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
123	28	oveq1d 7364	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝐴 − 𝐵))
124	68, 122, 123	3eqtr2d 2770	. 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 28606	. . . . 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 28603	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘𝐴)𝐼𝐴))
136	1, 2, 3, 10, 20, 125, 127, 21, 131	mirbtwn 28603	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘(𝑀‘𝐴))𝐼(𝑀‘𝐴)))
137		eqidd 2730	. . . . . . . . . . . 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 28724	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
142	141	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
143		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝑀‘𝐴))
144	143	oveq2d 7365	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀‘𝐴)))
145	142, 144	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼𝐴))
146	1, 2, 3, 138, 139, 140, 145	axtgbtwnid 28411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
147		eqidd 2730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = 𝐴)
148	137, 146, 147	s3eqd 14771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ = ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩)
149	1, 2, 3, 10, 20, 4, 18, 8, 8	ragtrivb 28647	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
150	149	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
151	148, 150	eqeltrrd 2829	. . . . . . . . . 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 2926	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ (𝑀‘𝐴) ↔ ¬ 𝐴 = (𝑀‘𝐴))
157	39	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴)))
158	157	orcomd 871	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = (𝑀‘𝐴) ∨ 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴))))
159	158	orcanai 1004	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐴 = (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)))
160	156, 159	sylan2b 594	. . . . . . . . . . . 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 28725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − 𝐴) = (𝐴 − (𝑀‘𝐴)))
170	169	eqcomd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − (𝑀‘𝐴)) = (𝐴 − 𝐴))
171	1, 2, 3, 164, 165, 166, 165, 170	axtgcgrid 28408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 = (𝑀‘𝐴))
172	171	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴 → 𝐴 = (𝑀‘𝐴)))
173	172	necon3d 2946	. . . . . . . . . . . . . . 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 28564	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐿(𝑀‘𝐴)))
177	1, 3, 10, 152, 155, 161, 162, 163, 174, 176	tglineelsb2 28577	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
178	1, 3, 10, 152, 163, 155, 174	tglinecom 28580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
179	177, 178	eqtr4d 2767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
180	160, 179	breqtrd 5118	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
181	1, 2, 3, 10, 152, 153, 154, 155, 180	perpdrag 28673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
182	151, 181	pm2.61dane 3012	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
183	1, 2, 3, 10, 20, 4, 18, 13, 8	israg 28642	. . . . . . . . 9 ⊢ (𝜑 → (⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))))
184	182, 183	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
185		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
186	1, 2, 3, 4, 7, 8, 12, 20, 13	ismidb 28723	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴))))
187	185, 186	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))
188	187	oveq2d 7365	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐴)) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
189	184, 188	eqtr4d 2767	. . . . . . 7 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
190	1, 2, 3, 10, 20, 4, 18, 21, 8	mircgr 28602	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
191	1, 2, 3, 10, 20, 4, 18, 21, 12	mircgr 28602	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘(𝑀‘𝐴))) = (𝑍 − (𝑀‘𝐴)))
192	189, 190, 191	3eqtr4d 2774	. . . . . 6 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
193	192	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
194	1, 2, 3, 125, 127, 126, 127, 130, 193	tgcgrcomlr 28425	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝑍) = ((𝑆‘(𝑀‘𝐴)) − 𝑍))
195	189	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
196	21	fveq1i 6823	. . . . . . . . . 10 ⊢ (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))
197	1, 2, 3, 4, 7, 8, 12, 21, 18	mirmid 28728	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
198	6	eqcomi 2738	. . . . . . . . . . 11 ⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍
199	1, 2, 3, 4, 7, 13, 16, 20, 18	ismidb 28723	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍))
200	198, 199	mpbiri 258	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
201	196, 197, 200	3eqtr4a 2790	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
202	1, 2, 3, 4, 7, 22, 129, 20, 16	ismidb 28723	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)) ↔ ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
203	201, 202	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)))
204	119, 203	oveq12d 7367	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))) = ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))))
205		eqid 2729	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵))) = ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))
206	1, 2, 3, 10, 20, 4, 16, 205, 14, 22	miriso 28615	. . . . . . 7 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))) = (𝐵 − (𝑆‘𝐴)))
207	204, 206	eqtr2d 2765	. . . . . 6 ⊢ (𝜑 → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
208	207	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
209	1, 2, 3, 125, 132, 126, 133, 130, 208	tgcgrcomlr 28425	. . . 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 28410	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐴 − 𝐵) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
212	211	eqcomd 2735	. 2 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))
213	124, 212	pm2.61dane 3012	1 ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5092 ran crn 5620 ‘cfv 6482 (class class class)co 7349 2c2 12183 ⟨“cs3 14749 Basecbs 17120 distcds 17170 TarskiGcstrkg 28372 Dim_TarskiG≥cstrkgld 28376 Itvcitv 28378 LineGclng 28379 pInvGcmir 28597 ∟Gcrag 28638 ⟂Gcperpg 28640 midGcmid 28717 lInvGclmi 28718

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-oadd 8392 df-er 8625 df-map 8755 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-xnn0 12458 df-z 12472 df-uz 12736 df-fz 13411 df-fzo 13558 df-hash 14238 df-word 14421 df-concat 14478 df-s1 14503 df-s2 14755 df-s3 14756 df-trkgc 28393 df-trkgb 28394 df-trkgcb 28395 df-trkgld 28397 df-trkg 28398 df-cgrg 28456 df-leg 28528 df-mir 28598 df-rag 28639 df-perpg 28641 df-mid 28719 df-lmi 28720

This theorem is referenced by: lmiiso 28742

W3C validator