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 28085

Description: Lemma for lmiiso 28086. (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 481	. . . . . . . 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 28075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃)
13	1, 2, 3, 4, 7, 8, 12	midcl 28066	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
14		lmiiso.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
15	1, 2, 3, 4, 7, 9, 10, 11, 14	lmicl 28075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃)
16	1, 2, 3, 4, 7, 14, 15	midcl 28066	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
17	1, 2, 3, 4, 7, 13, 16	midcl 28066	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ 𝑃)
18	6, 17	eqeltrid 2837	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19	18	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝑃)
20		eqid 2732	. . . . . . . . . 10 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
21		lmiisolem.s	. . . . . . . . . 10 ⊢ 𝑆 = ((pInvG‘𝐺)‘𝑍)
22	1, 2, 3, 10, 20, 4, 18, 21, 8	mircl 27950	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐴) ∈ 𝑃)
23	22	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) ∈ 𝑃)
24	8	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝑃)
25	1, 2, 3, 10, 20, 5, 19, 21, 24	mircgr 27946	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
26		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) = 𝑍)
27	26	eqcomd 2738	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = (𝑆‘𝐴))
28	1, 2, 3, 5, 19, 23, 19, 24, 25, 27	tgcgreq 27771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = 𝐴)
29		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
30	29	oveq2d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))))
31	6, 30	eqtr4id 2791	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))))
32	4	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺 ∈ TarskiG)
33	7	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺Dim_TarskiG≥2)
34	13	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
35	1, 2, 3, 32, 33, 34, 34	midid 28070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
36	31, 35	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
37		eqidd 2733	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀‘𝐴) = (𝑀‘𝐴))
38	1, 2, 3, 4, 7, 9, 10, 11, 8, 12	islmib 28076	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀‘𝐴) = (𝑀‘𝐴) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴)))))
39	37, 38	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴))))
40	39	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
41	40	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
42	36, 41	eqeltrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷)
43	4	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐺 ∈ TarskiG)
44	13	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
45	16	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
46	18	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝑃)
47		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵)))
48	1, 2, 3, 4, 7, 13, 16	midbtwn 28068	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
49	6, 48	eqeltrid 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
50	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐼(𝐵(midG‘𝐺)(𝑀‘𝐵))))
51	1, 3, 10, 43, 44, 45, 46, 47, 50	btwnlng1 27908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
52	11	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 ∈ ran 𝐿)
53	40	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
54		eqidd 2733	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀‘𝐵) = (𝑀‘𝐵))
55	1, 2, 3, 4, 7, 9, 10, 11, 14, 15	islmib 28076	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀‘𝐵) = (𝑀‘𝐵) ↔ ((𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵)))))
56	54, 55	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷 ∧ (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵))))
57	56	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷)
58	57	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷)
59	1, 3, 10, 43, 44, 45, 47, 47, 52, 53, 58	tglinethru 27925	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝐷 = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
60	51, 59	eleqtrrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ (𝐵(midG‘𝐺)(𝑀‘𝐵))) → 𝑍 ∈ 𝐷)
61	42, 60	pm2.61dane 3029	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ 𝐷)
62	61	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 ∈ 𝐷)
63	28, 62	eqeltrrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝐷)
64	1, 2, 3, 4, 7, 9, 10, 11, 8	lmiinv 28081	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷))
65	64	biimpar 478	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐷) → (𝑀‘𝐴) = 𝐴)
66	63, 65	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝐴)
67	66, 28	eqtr4d 2775	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝑍)
68	67	oveq1d 7426	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝑍 − (𝑀‘𝐵)))
69		eqidd 2733	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝑍 = 𝑍)
70	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐺 ∈ TarskiG)
71	14	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 ∈ 𝑃)
72	16	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
73	1, 2, 3, 4, 7, 14, 15	midbtwn 28068	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
74	73	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
75		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝑀‘𝐵))
76	75	oveq2d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀‘𝐵)))
77	74, 76	eleqtrrd 2836	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼𝐵))
78	1, 2, 3, 70, 71, 72, 77	axtgbtwnid 27755	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
79		eqidd 2733	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = 𝐵)
80	69, 78, 79	s3eqd 14817	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ = ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩)
81	1, 2, 3, 10, 20, 4, 18, 14, 14	ragtrivb 27991	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
82	81	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ ∈ (∟G‘𝐺))
83	80, 82	eqeltrrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
84	4	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐺 ∈ TarskiG)
85	61	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝑍 ∈ 𝐷)
86	57	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝐷)
87	14	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐵 ∈ 𝑃)
88		df-ne 2941	. . . . . . . . . 10 ⊢ (𝐵 ≠ (𝑀‘𝐵) ↔ ¬ 𝐵 = (𝑀‘𝐵))
89	56	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)) ∨ 𝐵 = (𝑀‘𝐵)))
90	89	orcomd 869	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 = (𝑀‘𝐵) ∨ 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵))))
91	90	orcanai 1001	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)))
92	88, 91	sylan2b 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)(𝐵𝐿(𝑀‘𝐵)))
93	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝑀‘𝐵) ∈ 𝑃)
94		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐵 ≠ (𝑀‘𝐵))
95	16	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
96	4	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐺 ∈ TarskiG)
97	14	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 ∈ 𝑃)
98	15	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝑀‘𝐵) ∈ 𝑃)
99	7	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐺Dim_TarskiG≥2)
100		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵)
101	1, 2, 3, 96, 99, 97, 98, 100	midcgr 28069	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − 𝐵) = (𝐵 − (𝑀‘𝐵)))
102	101	eqcomd 2738	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − (𝑀‘𝐵)) = (𝐵 − 𝐵))
103	1, 2, 3, 96, 97, 98, 97, 102	axtgcgrid 27752	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → 𝐵 = (𝑀‘𝐵))
104	103	ex 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵 → 𝐵 = (𝑀‘𝐵)))
105	104	necon3d 2961	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ≠ (𝑀‘𝐵) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ≠ 𝐵))
106	105	imp 407	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ≠ 𝐵)
107	73	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
108	1, 3, 10, 84, 87, 93, 95, 94, 107	btwnlng1 27908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐿(𝑀‘𝐵)))
109	1, 3, 10, 84, 87, 93, 94, 95, 106, 108	tglineelsb2 27921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
110	1, 3, 10, 84, 95, 87, 106	tglinecom 27924	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
111	109, 110	eqtr4d 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
112	92, 111	breqtrd 5174	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
113	1, 2, 3, 10, 84, 85, 86, 87, 112	perpdrag 28017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
114	83, 113	pm2.61dane 3029	. . . . . 6 ⊢ (𝜑 → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
115	1, 2, 3, 10, 20, 4, 18, 16, 14	israg 27986	. . . . . 6 ⊢ (𝜑 → (⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))))
116	114, 115	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
117		eqidd 2733	. . . . . . 7 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
118	1, 2, 3, 4, 7, 14, 15, 20, 16	ismidb 28067	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
119	117, 118	mpbird 256	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))
120	119	oveq2d 7427	. . . . 5 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐵)) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
121	116, 120	eqtr4d 2775	. . . 4 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
122	121	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
123	28	oveq1d 7426	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝐴 − 𝐵))
124	68, 122, 123	3eqtr2d 2778	. 2 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))
125	4	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐺 ∈ TarskiG)
126	22	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘𝐴) ∈ 𝑃)
127	18	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ 𝑃)
128	8	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐴 ∈ 𝑃)
129	1, 2, 3, 10, 20, 4, 18, 21, 12	mircl 27950	. . . . 5 ⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) ∈ 𝑃)
130	129	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘(𝑀‘𝐴)) ∈ 𝑃)
131	12	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑀‘𝐴) ∈ 𝑃)
132	14	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝐵 ∈ 𝑃)
133	15	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑀‘𝐵) ∈ 𝑃)
134		simpr 485	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑆‘𝐴) ≠ 𝑍)
135	1, 2, 3, 10, 20, 125, 127, 21, 128	mirbtwn 27947	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘𝐴)𝐼𝐴))
136	1, 2, 3, 10, 20, 125, 127, 21, 131	mirbtwn 27947	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘(𝑀‘𝐴))𝐼(𝑀‘𝐴)))
137		eqidd 2733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝑍 = 𝑍)
138	4	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐺 ∈ TarskiG)
139	8	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 ∈ 𝑃)
140	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
141	1, 2, 3, 4, 7, 8, 12	midbtwn 28068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
142	141	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
143		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝑀‘𝐴))
144	143	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀‘𝐴)))
145	142, 144	eleqtrrd 2836	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼𝐴))
146	1, 2, 3, 138, 139, 140, 145	axtgbtwnid 27755	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
147		eqidd 2733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = 𝐴)
148	137, 146, 147	s3eqd 14817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ = ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩)
149	1, 2, 3, 10, 20, 4, 18, 8, 8	ragtrivb 27991	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
150	149	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ ∈ (∟G‘𝐺))
151	148, 150	eqeltrrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
152	4	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐺 ∈ TarskiG)
153	61	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝑍 ∈ 𝐷)
154	40	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝐷)
155	8	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐴 ∈ 𝑃)
156		df-ne 2941	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ (𝑀‘𝐴) ↔ ¬ 𝐴 = (𝑀‘𝐴))
157	39	simprd 496	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)) ∨ 𝐴 = (𝑀‘𝐴)))
158	157	orcomd 869	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 = (𝑀‘𝐴) ∨ 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴))))
159	158	orcanai 1001	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐴 = (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)))
160	156, 159	sylan2b 594	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿(𝑀‘𝐴)))
161	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝑀‘𝐴) ∈ 𝑃)
162		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐴 ≠ (𝑀‘𝐴))
163	13	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
164	4	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐺 ∈ TarskiG)
165	8	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 ∈ 𝑃)
166	12	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝑀‘𝐴) ∈ 𝑃)
167	7	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐺Dim_TarskiG≥2)
168		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴)
169	1, 2, 3, 164, 167, 165, 166, 168	midcgr 28069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − 𝐴) = (𝐴 − (𝑀‘𝐴)))
170	169	eqcomd 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − (𝑀‘𝐴)) = (𝐴 − 𝐴))
171	1, 2, 3, 164, 165, 166, 165, 170	axtgcgrid 27752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → 𝐴 = (𝑀‘𝐴))
172	171	ex 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴 → 𝐴 = (𝑀‘𝐴)))
173	172	necon3d 2961	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ≠ (𝑀‘𝐴) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ 𝐴))
174	173	imp 407	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ≠ 𝐴)
175	141	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
176	1, 3, 10, 152, 155, 161, 163, 162, 175	btwnlng1 27908	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐿(𝑀‘𝐴)))
177	1, 3, 10, 152, 155, 161, 162, 163, 174, 176	tglineelsb2 27921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
178	1, 3, 10, 152, 163, 155, 174	tglinecom 27924	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
179	177, 178	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
180	160, 179	breqtrd 5174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
181	1, 2, 3, 10, 152, 153, 154, 155, 180	perpdrag 28017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
182	151, 181	pm2.61dane 3029	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
183	1, 2, 3, 10, 20, 4, 18, 13, 8	israg 27986	. . . . . . . . 9 ⊢ (𝜑 → (⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))))
184	182, 183	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
185		eqidd 2733	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
186	1, 2, 3, 4, 7, 8, 12, 20, 13	ismidb 28067	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴))))
187	185, 186	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))
188	187	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐴)) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
189	184, 188	eqtr4d 2775	. . . . . . 7 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
190	1, 2, 3, 10, 20, 4, 18, 21, 8	mircgr 27946	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
191	1, 2, 3, 10, 20, 4, 18, 21, 12	mircgr 27946	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘(𝑀‘𝐴))) = (𝑍 − (𝑀‘𝐴)))
192	189, 190, 191	3eqtr4d 2782	. . . . . 6 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
193	192	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
194	1, 2, 3, 125, 127, 126, 127, 130, 193	tgcgrcomlr 27769	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝑍) = ((𝑆‘(𝑀‘𝐴)) − 𝑍))
195	189	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
196	21	fveq1i 6892	. . . . . . . . . 10 ⊢ (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))
197	1, 2, 3, 4, 7, 8, 12, 21, 18	mirmid 28072	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
198	6	eqcomi 2741	. . . . . . . . . . 11 ⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍
199	1, 2, 3, 4, 7, 13, 16, 20, 18	ismidb 28067	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))) ↔ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍))
200	198, 199	mpbiri 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (((pInvG‘𝐺)‘𝑍)‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
201	196, 197, 200	3eqtr4a 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
202	1, 2, 3, 4, 7, 22, 129, 20, 16	ismidb 28067	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)) ↔ ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
203	201, 202	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)))
204	119, 203	oveq12d 7429	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))) = ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))))
205		eqid 2732	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵))) = ((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))
206	1, 2, 3, 10, 20, 4, 16, 205, 14, 22	miriso 27959	. . . . . . 7 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴))) = (𝐵 − (𝑆‘𝐴)))
207	204, 206	eqtr2d 2773	. . . . . 6 ⊢ (𝜑 → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
208	207	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐵 − (𝑆‘𝐴)) = ((𝑀‘𝐵) − (𝑆‘(𝑀‘𝐴))))
209	1, 2, 3, 125, 132, 126, 133, 130, 208	tgcgrcomlr 27769	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑆‘𝐴) − 𝐵) = ((𝑆‘(𝑀‘𝐴)) − (𝑀‘𝐵)))
210	121	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
211	1, 2, 3, 125, 126, 127, 128, 130, 127, 131, 132, 133, 134, 135, 136, 194, 195, 209, 210	axtg5seg 27754	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝐴 − 𝐵) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
212	211	eqcomd 2738	. 2 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))
213	124, 212	pm2.61dane 3029	1 ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 class class class wbr 5148 ran crn 5677 ‘cfv 6543 (class class class)co 7411 2c2 12269 ⟨“cs3 14795 Basecbs 17146 distcds 17208 TarskiGcstrkg 27716 Dim_TarskiG≥cstrkgld 27720 Itvcitv 27722 LineGclng 27723 pInvGcmir 27941 ∟Gcrag 27982 ⟂Gcperpg 27984 midGcmid 28061 lInvGclmi 28062

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-dju 9898 df-card 9936 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-nn 12215 df-2 12277 df-3 12278 df-n0 12475 df-xnn0 12547 df-z 12561 df-uz 12825 df-fz 13487 df-fzo 13630 df-hash 14293 df-word 14467 df-concat 14523 df-s1 14548 df-s2 14801 df-s3 14802 df-trkgc 27737 df-trkgb 27738 df-trkgcb 27739 df-trkgld 27741 df-trkg 27742 df-cgrg 27800 df-leg 27872 df-mir 27942 df-rag 27983 df-perpg 27985 df-mid 28063 df-lmi 28064

This theorem is referenced by: lmiiso 28086

W3C validator