angmgmaddrid - Metamath Proof Explorer

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

Theorem angmgmaddrid 29327

Description: The right identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)

**Hypotheses**
Ref	Expression
angmgmadd.p	⊢ 𝑃 = (Base‘𝐺)
angmgmadd.a	⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}
angmgmadd.i	⊢ 𝐼 = (Itv‘𝐺)
angmgmadd.d	⊢ − = (dist‘𝐺)
angmgmadd.c	⊢ ∼ = (cgrA‘𝐺)
angmgmadd.l	⊢ 𝐿 = (LineG‘𝐺)
angmgmadd.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
angmgmadd.o	⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))
angmgmaddlid.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
angmgmaddlid.y	⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))
angmgmaddlid.e	⊢ (𝜑 → 𝐸 ∈ 𝐴)

**Assertion**
Ref	Expression
angmgmaddrid	⊢ (𝜑 → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)

Distinct variable groups: − ,𝑑,𝑒,𝑓,𝑠 ∼ ,𝑠 𝐸,𝑑,𝑒,𝑓,𝑠 𝐺,𝑑,𝑒,𝑓,𝑠 𝐼,𝑑,𝑒,𝑓,𝑠 𝐿,𝑑,𝑒,𝑓,𝑠 𝑃,𝑑,𝑒,𝑓,𝑠 𝑋,𝑑,𝑒,𝑓,𝑠 𝑌,𝑑,𝑒,𝑓,𝑠 𝜑,𝑑,𝑒,𝑓,𝑠 Allowed substitution hints: 𝐴(𝑒, 𝑓, 𝑠, 𝑑) + (𝑒, 𝑓, 𝑠, 𝑑) ∼ (𝑒, 𝑓, 𝑑)

Proof of Theorem angmgmaddrid Dummy variables 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp-8r 804	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
2	1	oveq1d 7423	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩))
3		angmgmadd.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Base‘𝐺)
4		angmgmadd.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))}
5		angmgmadd.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (Itv‘𝐺)
6		angmgmadd.d	. . . . . . . . . . . . 13 ⊢ − = (dist‘𝐺)
7		angmgmadd.c	. . . . . . . . . . . . 13 ⊢ ∼ = (cgrA‘𝐺)
8		angmgmadd.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LineG‘𝐺)
9		angmgmadd.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
10	9	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝐺 ∈ TarskiG)
11	10	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝐺 ∈ TarskiG)
12		angmgmaddlid.x	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
13	12	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑋 ∈ 𝑃)
14	13	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋 ∈ 𝑃)
15		angmgmaddlid.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋}))
16	15	eldifad 3910	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17	16	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑌 ∈ 𝑃)
18	17	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ∈ 𝑃)
19		simp-7r 802	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑢 ∈ 𝑃)
20	19	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ∈ 𝑃)
21		simp-6r 800	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ∈ 𝑃)
22	21	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ∈ 𝑃)
23		simp-5r 798	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ∈ 𝑃)
24	23	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤 ∈ 𝑃)
25	15	eldifsnbd 4748	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
26	25	necomd 3010	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
27	26	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑋 ≠ 𝑌)
28	27	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋 ≠ 𝑌)
29	25	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑌 ≠ 𝑋)
30	29	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ≠ 𝑋)
31		simpllr 788	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑢 ≠ 𝑣)
32	31	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ≠ 𝑣)
33		simp-6r 800	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ≠ 𝑤)
34		angmgmadd.o	. . . . . . . . . . . . 13 ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩))
35		simp-5r 798	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ∈ (𝑣𝐿𝑤))
36		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡 ∈ 𝑃)
37		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
38		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡((hlG‘𝐺)‘𝑌)𝑋)
39	3, 5, 37, 36, 14, 18, 11, 38	hlcomd 29004	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋((hlG‘𝐺)‘𝑌)𝑡)
40		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤((hlG‘𝐺)‘𝑣)𝑢)
41	3, 5, 37, 24, 20, 22, 11, 40	hlcomd 29004	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢((hlG‘𝐺)‘𝑣)𝑤)
42	3, 7, 37, 11, 39, 41, 18, 22	zerocgra 29265	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → ⟨“𝑋𝑌𝑡”⟩ ∼ ⟨“𝑢𝑣𝑤”⟩)
43		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝑌 − 𝑡) = (𝑣 − 𝑢))
44	3, 4, 5, 6, 7, 8, 11, 14, 18, 14, 20, 22, 24, 28, 30, 32, 33, 34, 35, 36, 42, 43	angmgmaddov2 29323	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
45	2, 44	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
46	45, 42	eqbrtrd 5126	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
47	46	anasss 472	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡((hlG‘𝐺)‘𝑌)𝑋 ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
48	16	ad8antr 753	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑌 ∈ 𝑃)
49	21	adantr 486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑣 ∈ 𝑃)
50	19	adantr 486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑢 ∈ 𝑃)
51	10	adantr 486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝐺 ∈ TarskiG)
52	13	adantr 486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑋 ∈ 𝑃)
53	26	ad8antr 753	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑋 ≠ 𝑌)
54	31	adantr 486	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑢 ≠ 𝑣)
55	54	necomd 3010	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑣 ≠ 𝑢)
56	3, 5, 37, 48, 49, 50, 51, 52, 6, 53, 55	hlcgrex 29016	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → ∃𝑡 ∈ 𝑃 (𝑡((hlG‘𝐺)‘𝑌)𝑋 ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)))
57	47, 56	r19.29a 3170	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
58		simp-8r 804	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
59	58	oveq1d 7423	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩))
60	10	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → 𝐺 ∈ TarskiG)
61	60	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝐺 ∈ TarskiG)
62	13	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → 𝑋 ∈ 𝑃)
63	62	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋 ∈ 𝑃)
64	16	ad8antr 753	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → 𝑌 ∈ 𝑃)
65	64	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ∈ 𝑃)
66	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → 𝑢 ∈ 𝑃)
67	66	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ∈ 𝑃)
68	21	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → 𝑣 ∈ 𝑃)
69	68	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ∈ 𝑃)
70	23	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤 ∈ 𝑃)
71	27	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋 ≠ 𝑌)
72	71	necomd 3010	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ≠ 𝑋)
73	31	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ≠ 𝑣)
74		simp-6r 800	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ≠ 𝑤)
75		simp-5r 798	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ∈ (𝑣𝐿𝑤))
76		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡 ∈ 𝑃)
77	7	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ (cgrA‘𝐺) = ∼
78	77	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (cgrA‘𝐺) = ∼ )
79		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ∈ (𝑋𝐼𝑡))
80		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ∈ (𝑢𝐼𝑤))
81		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝑌 − 𝑡) = (𝑣 − 𝑢))
82	81	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝑣 − 𝑢) = (𝑌 − 𝑡))
83	73	necomd 3010	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ≠ 𝑢)
84	3, 6, 5, 61, 69, 67, 65, 76, 82, 83	tgcgrneq 28879	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ≠ 𝑡)
85	84	necomd 3010	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡 ≠ 𝑌)
86	74	necomd 3010	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤 ≠ 𝑣)
87	3, 5, 6, 61, 63, 65, 76, 67, 69, 70, 79, 80, 71, 85, 73, 86	flatcgra 29266	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → ⟨“𝑋𝑌𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑤”⟩)
88	78, 87	breqdi 5117	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → ⟨“𝑋𝑌𝑡”⟩ ∼ ⟨“𝑢𝑣𝑤”⟩)
89	3, 4, 5, 6, 7, 8, 61, 63, 65, 63, 67, 69, 70, 71, 72, 73, 74, 34, 75, 76, 88, 81	angmgmaddov2 29323	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
90	59, 89	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
91	90, 88	eqbrtrd 5126	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
92	91	anasss 472	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑌 ∈ (𝑋𝐼𝑡) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
93	3, 6, 5, 60, 62, 64, 68, 66	axtgsegcon 28860	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → ∃𝑡 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑡) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)))
94	92, 93	r19.29a 3170	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
95		simpr 490	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑢 ∈ (𝑣𝐿𝑤))
96		simplr 781	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ≠ 𝑤)
97	3, 5, 8, 10, 19, 21, 23, 31, 95, 96	lnrot2 29026	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ∈ (𝑢𝐿𝑣))
98	3, 5, 37, 19, 21, 23, 10, 13, 8, 97	lnhl 29015	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝑤((hlG‘𝐺)‘𝑣)𝑢 ∨ 𝑣 ∈ (𝑢𝐼𝑤)))
99	57, 94, 98	mpjaodan 973	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
100		simp-7r 802	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
101	100	oveq1d 7423	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩))
102	9	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝐺 ∈ TarskiG)
103	102	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝐺 ∈ TarskiG)
104	12	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑋 ∈ 𝑃)
105	104	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑋 ∈ 𝑃)
106	16	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑌 ∈ 𝑃)
107	106	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑌 ∈ 𝑃)
108		simp-10r 808	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑢 ∈ 𝑃)
109		simp-6r 800	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ∈ 𝑃)
110	109	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑣 ∈ 𝑃)
111		simp-5r 798	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ∈ 𝑃)
112	111	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑤 ∈ 𝑃)
113	26	ad10antr 757	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑋 ≠ 𝑌)
114	25	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑌 ≠ 𝑋)
115	114	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑌 ≠ 𝑋)
116		simp-6r 800	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑢 ≠ 𝑣)
117		simp-5r 798	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑣 ≠ 𝑤)
118		simp-4r 796	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ¬ 𝑢 ∈ (𝑣𝐿𝑤))
119		simpllr 788	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ 𝑃)
120		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡((hlG‘𝐺)‘𝑣)𝑤)
121	3, 5, 37, 119, 112, 110, 103, 120	hlcomd 29004	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑤((hlG‘𝐺)‘𝑣)𝑡)
122	3, 5, 37, 105, 105, 107, 103, 113	hlid 29009	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑋((hlG‘𝐺)‘𝑌)𝑋)
123	3, 7, 37, 103, 121, 122, 110, 107	zerocgra 29265	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑤𝑣𝑡”⟩ ∼ ⟨“𝑋𝑌𝑋”⟩)
124		simpr 490	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝑣 − 𝑡) = (𝑌 − 𝑋))
125	3, 5, 37, 112, 119, 110, 103, 8, 121	hlln 29007	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑤 ∈ (𝑡𝐿𝑣))
126	3, 8, 5, 103, 119, 110, 125	tglngne 28947	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ≠ 𝑣)
127	3, 5, 8, 103, 110, 112, 119, 117, 125, 126	lnrot1 29025	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ (𝑣𝐿𝑤))
128	3, 6, 5, 103, 119, 108	tgbtwntriv1 28888	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ (𝑡𝐼𝑢))
129	127, 128	elind 4145	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ ((𝑣𝐿𝑤) ∩ (𝑡𝐼𝑢)))
130	129	ne0d 4287	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ((𝑣𝐿𝑤) ∩ (𝑡𝐼𝑢)) ≠ ∅)
131	3, 4, 5, 6, 7, 8, 103, 105, 107, 105, 108, 110, 112, 113, 115, 116, 117, 34, 118, 119, 123, 124, 130	angmgmaddov1 29322	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑢𝑣𝑡”⟩)
132	101, 131	eqtrd 2795	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑢𝑣𝑡”⟩)
133	77	a1i 11	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (cgrA‘𝐺) = ∼ )
134	126	necomd 3010	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑣 ≠ 𝑡)
135	3, 5, 103, 37, 108, 110, 119, 116, 134	cgraid 29260	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑡”⟩)
136	3, 5, 37, 103, 108, 110, 119, 108, 110, 119, 135, 112, 121	cgrahl2 29258	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑤”⟩)
137	133, 136	breqdi 5117	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩ ∼ ⟨“𝑢𝑣𝑤”⟩)
138	132, 137	eqbrtrd 5126	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
139	138	anasss 472	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡((hlG‘𝐺)‘𝑣)𝑤 ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
140		simplr 781	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ≠ 𝑤)
141	140	necomd 3010	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ≠ 𝑣)
142	3, 5, 37, 109, 106, 104, 102, 111, 6, 141, 114	hlcgrex 29016	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → ∃𝑡 ∈ 𝑃 (𝑡((hlG‘𝐺)‘𝑣)𝑤 ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)))
143	139, 142	r19.29a 3170	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
144	99, 143	pm2.61dan 825	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
145		simpllr 788	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
146	144, 145	breqtrrd 5132	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
147	146	anasss 472	. . . 4 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
148	147	anasss 472	. . 3 ⊢ (((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
149	148	r19.29an 3166	. 2 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ ∃𝑤 ∈ 𝑃 (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
150	3	fvexi 6887	. . 3 ⊢ 𝑃 ∈ V
151		angmgmaddlid.e	. . 3 ⊢ (𝜑 → 𝐸 ∈ 𝐴)
152	150, 4, 151	elcgrabasi 29309	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤)))
153	149, 152	r19.29vva 3222	1 ⊢ (𝜑 → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∃wrex 3086 {crab 3412 ∖ cdif 3895 ∩ cin 3897 ∅c0 4278 ifcif 4481 {csn 4583 class class class wbr 5102 ‘cfv 6527 ℩crio 7364 (class class class)co 7408 ∈ cmpo 7410 ↑_m cmap 8825 0cc0 11172 1c1 11173 2c2 12367 3c3 12368 ..^cfzo 13757 ⟨“cs3 14961 Basecbs 17349 distcds 17399 TarskiGcstrkg 28823 Itvcitv 28829 LineGclng 28830 hlGchlg 28997 cgrAccgra 29248

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248 ax-pre-mulgt0 11249

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-oadd 8458 df-er 8695 df-map 8827 df-pm 8828 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-dju 9954 df-card 9992 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516 df-nn 12306 df-2 12375 df-3 12376 df-n0 12577 df-xnn0 12650 df-z 12664 df-uz 12936 df-fz 13610 df-fzo 13758 df-hash 14443 df-word 14627 df-concat 14684 df-s1 14711 df-s2 14967 df-s3 14968 df-trkgc 28844 df-trkgb 28845 df-trkgcb 28846 df-trkgld 28848 df-trkg 28849 df-cgrg 28908 df-ismt 28930 df-leg 28980 df-hlg 28998 df-mir 29059 df-rag 29103 df-perpg 29105 df-hpg 29170 df-mid 29213 df-lmi 29214 df-cgra 29249

This theorem is used by: angmgmlem 29329

W3C validator