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 28776

Description: Lemma for lmiiso 28777. (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 28766	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑃)
13	1, 2, 3, 4, 7, 8, 12	midcl 28757	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ 𝑃)
14		lmiiso.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
15	1, 2, 3, 4, 7, 9, 10, 11, 14	lmicl 28766	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀‘𝐵) ∈ 𝑃)
16	1, 2, 3, 4, 7, 14, 15	midcl 28757	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ 𝑃)
17	1, 2, 3, 4, 7, 13, 16	midcl 28757	. . . . . . . . . 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 28641	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐴) ∈ 𝑃)
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) ∈ 𝑃)
24	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝐴 ∈ 𝑃)
25	1, 2, 3, 10, 20, 5, 19, 21, 24	mircgr 28637	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
26		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑆‘𝐴) = 𝑍)
27	26	eqcomd 2735	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = (𝑆‘𝐴))
28	1, 2, 3, 5, 19, 23, 19, 24, 25, 27	tgcgreq 28462	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → 𝑍 = 𝐴)
29		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
30	29	oveq2d 7385	. . . . . . . . . . . 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 28761	. . . . . . . . . . 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 28767	. . . . . . . . . . . . 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 28759	. . . . . . . . . . . . 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 28599	. . . . . . . . . 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 28767	. . . . . . . . . . . . . 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 28616	. . . . . . . . . 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 28772	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐴) = 𝐴 ↔ 𝐴 ∈ 𝐷))
65	64	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝐷) → (𝑀‘𝐴) = 𝐴)
66	63, 65	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝐴)
67	66, 28	eqtr4d 2767	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑀‘𝐴) = 𝑍)
68	67	oveq1d 7384	. . 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 28759	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
74	73	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼(𝑀‘𝐵)))
75		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝑀‘𝐵))
76	75	oveq2d 7385	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵𝐼𝐵) = (𝐵𝐼(𝑀‘𝐵)))
77	74, 76	eleqtrrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐼𝐵))
78	1, 2, 3, 70, 71, 72, 77	axtgbtwnid 28446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = (𝐵(midG‘𝐺)(𝑀‘𝐵)))
79		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → 𝐵 = 𝐵)
80	69, 78, 79	s3eqd 14806	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = (𝑀‘𝐵)) → ⟨“𝑍𝐵𝐵”⟩ = ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩)
81	1, 2, 3, 10, 20, 4, 18, 14, 14	ragtrivb 28682	. . . . . . . . 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 28760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − 𝐵) = (𝐵 − (𝑀‘𝐵)))
102	101	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = 𝐵) → (𝐵 − (𝑀‘𝐵)) = (𝐵 − 𝐵))
103	1, 2, 3, 96, 97, 98, 97, 102	axtgcgrid 28443	. . . . . . . . . . . . . 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 28599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵(midG‘𝐺)(𝑀‘𝐵)) ∈ (𝐵𝐿(𝑀‘𝐵)))
109	1, 3, 10, 84, 87, 93, 94, 95, 106, 108	tglineelsb2 28612	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
110	1, 3, 10, 84, 95, 87, 106	tglinecom 28615	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵) = (𝐵𝐿(𝐵(midG‘𝐺)(𝑀‘𝐵))))
111	109, 110	eqtr4d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → (𝐵𝐿(𝑀‘𝐵)) = ((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
112	92, 111	breqtrd 5128	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → 𝐷(⟂G‘𝐺)((𝐵(midG‘𝐺)(𝑀‘𝐵))𝐿𝐵))
113	1, 2, 3, 10, 84, 85, 86, 87, 112	perpdrag 28708	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ (𝑀‘𝐵)) → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
114	83, 113	pm2.61dane 3012	. . . . . 6 ⊢ (𝜑 → ⟨“𝑍(𝐵(midG‘𝐺)(𝑀‘𝐵))𝐵”⟩ ∈ (∟G‘𝐺))
115	1, 2, 3, 10, 20, 4, 18, 16, 14	israg 28677	. . . . . 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 28758	. . . . . . 7 ⊢ (𝜑 → ((𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵) ↔ (𝐵(midG‘𝐺)(𝑀‘𝐵)) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
119	117, 118	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐵) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵))
120	119	oveq2d 7385	. . . . 5 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐵)) = (𝑍 − (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘𝐵)))
121	116, 120	eqtr4d 2767	. . . 4 ⊢ (𝜑 → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
122	121	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑆‘𝐴) = 𝑍) → (𝑍 − 𝐵) = (𝑍 − (𝑀‘𝐵)))
123	28	oveq1d 7384	. . 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 28641	. . . . 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 28638	. . . 4 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → 𝑍 ∈ ((𝑆‘𝐴)𝐼𝐴))
136	1, 2, 3, 10, 20, 125, 127, 21, 131	mirbtwn 28638	. . . 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 28759	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
142	141	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼(𝑀‘𝐴)))
143		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝑀‘𝐴))
144	143	oveq2d 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴𝐼𝐴) = (𝐴𝐼(𝑀‘𝐴)))
145	142, 144	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐼𝐴))
146	1, 2, 3, 138, 139, 140, 145	axtgbtwnid 28446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = (𝐴(midG‘𝐺)(𝑀‘𝐴)))
147		eqidd 2730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → 𝐴 = 𝐴)
148	137, 146, 147	s3eqd 14806	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 = (𝑀‘𝐴)) → ⟨“𝑍𝐴𝐴”⟩ = ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩)
149	1, 2, 3, 10, 20, 4, 18, 8, 8	ragtrivb 28682	. . . . . . . . . . . 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 28760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − 𝐴) = (𝐴 − (𝑀‘𝐴)))
170	169	eqcomd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = 𝐴) → (𝐴 − (𝑀‘𝐴)) = (𝐴 − 𝐴))
171	1, 2, 3, 164, 165, 166, 165, 170	axtgcgrid 28443	. . . . . . . . . . . . . . . . 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 28599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴(midG‘𝐺)(𝑀‘𝐴)) ∈ (𝐴𝐿(𝑀‘𝐴)))
177	1, 3, 10, 152, 155, 161, 162, 163, 174, 176	tglineelsb2 28612	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
178	1, 3, 10, 152, 163, 155, 174	tglinecom 28615	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴) = (𝐴𝐿(𝐴(midG‘𝐺)(𝑀‘𝐴))))
179	177, 178	eqtr4d 2767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → (𝐴𝐿(𝑀‘𝐴)) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
180	160, 179	breqtrd 5128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → 𝐷(⟂G‘𝐺)((𝐴(midG‘𝐺)(𝑀‘𝐴))𝐿𝐴))
181	1, 2, 3, 10, 152, 153, 154, 155, 180	perpdrag 28708	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐴 ≠ (𝑀‘𝐴)) → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
182	151, 181	pm2.61dane 3012	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝑍(𝐴(midG‘𝐺)(𝑀‘𝐴))𝐴”⟩ ∈ (∟G‘𝐺))
183	1, 2, 3, 10, 20, 4, 18, 13, 8	israg 28677	. . . . . . . . 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 28758	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴) ↔ (𝐴(midG‘𝐺)(𝑀‘𝐴)) = (𝐴(midG‘𝐺)(𝑀‘𝐴))))
187	185, 186	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘𝐴) = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴))
188	187	oveq2d 7385	. . . . . . . 8 ⊢ (𝜑 → (𝑍 − (𝑀‘𝐴)) = (𝑍 − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)(𝑀‘𝐴)))‘𝐴)))
189	184, 188	eqtr4d 2767	. . . . . . 7 ⊢ (𝜑 → (𝑍 − 𝐴) = (𝑍 − (𝑀‘𝐴)))
190	1, 2, 3, 10, 20, 4, 18, 21, 8	mircgr 28637	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − 𝐴))
191	1, 2, 3, 10, 20, 4, 18, 21, 12	mircgr 28637	. . . . . . 7 ⊢ (𝜑 → (𝑍 − (𝑆‘(𝑀‘𝐴))) = (𝑍 − (𝑀‘𝐴)))
192	189, 190, 191	3eqtr4d 2774	. . . . . 6 ⊢ (𝜑 → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
193	192	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑆‘𝐴) ≠ 𝑍) → (𝑍 − (𝑆‘𝐴)) = (𝑍 − (𝑆‘(𝑀‘𝐴))))
194	1, 2, 3, 125, 127, 126, 127, 130, 193	tgcgrcomlr 28460	. . . 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 28763	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝑆‘(𝐴(midG‘𝐺)(𝑀‘𝐴))))
198	6	eqcomi 2738	. . . . . . . . . . 11 ⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = 𝑍
199	1, 2, 3, 4, 7, 13, 16, 20, 18	ismidb 28758	. . . . . . . . . . 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 28758	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)) ↔ ((𝑆‘𝐴)(midG‘𝐺)(𝑆‘(𝑀‘𝐴))) = (𝐵(midG‘𝐺)(𝑀‘𝐵))))
203	201, 202	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝑀‘𝐴)) = (((pInvG‘𝐺)‘(𝐵(midG‘𝐺)(𝑀‘𝐵)))‘(𝑆‘𝐴)))
204	119, 203	oveq12d 7387	. . . . . . 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 28650	. . . . . . 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 28460	. . . 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 28445	. . 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 5102 ran crn 5632 ‘cfv 6499 (class class class)co 7369 2c2 12217 ⟨“cs3 14784 Basecbs 17155 distcds 17205 TarskiGcstrkg 28407 Dim_TarskiG≥cstrkgld 28411 Itvcitv 28413 LineGclng 28414 pInvGcmir 28632 ∟Gcrag 28673 ⟂Gcperpg 28675 midGcmid 28752 lInvGclmi 28753

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 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

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 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 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 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-oadd 8415 df-er 8648 df-map 8778 df-pm 8779 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-dju 9830 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-xnn0 12492 df-z 12506 df-uz 12770 df-fz 13445 df-fzo 13592 df-hash 14272 df-word 14455 df-concat 14512 df-s1 14537 df-s2 14790 df-s3 14791 df-trkgc 28428 df-trkgb 28429 df-trkgcb 28430 df-trkgld 28432 df-trkg 28433 df-cgrg 28491 df-leg 28563 df-mir 28633 df-rag 28674 df-perpg 28676 df-mid 28754 df-lmi 28755

This theorem is referenced by: lmiiso 28777

W3C validator