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 29273

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 7431	. . . . . . . . . . . 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 3914	. . . . . . . . . . . . . . 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 4752	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
26	25	necomd 3012	. . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . 14 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
38		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡((hlG‘𝐺)‘𝑌)𝑋)
39	3, 5, 37, 36, 14, 18, 11, 38	hlcomd 28950	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑋((hlG‘𝐺)‘𝑌)𝑡)
40		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤((hlG‘𝐺)‘𝑣)𝑢)
41	3, 5, 37, 24, 20, 22, 11, 40	hlcomd 28950	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢((hlG‘𝐺)‘𝑣)𝑤)
42	3, 7, 37, 11, 39, 41, 18, 22	zerocgra 29211	. . . . . . . . . . . . 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 29269	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
45	2, 44	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑌)𝑋) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
46	45, 42	eqbrtrd 5131	. . . . . . . . . 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 3012	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → 𝑣 ≠ 𝑢)
56	3, 5, 37, 48, 49, 50, 51, 52, 6, 53, 55	hlcgrex 28962	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → ∃𝑡 ∈ 𝑃 (𝑡((hlG‘𝐺)‘𝑌)𝑋 ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)))
57	47, 56	r19.29a 3172	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑤((hlG‘𝐺)‘𝑣)𝑢) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
58		simp-8r 804	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
59	58	oveq1d 7431	. . . . . . . . . . . 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 3012	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ≠ 𝑋)
73	31	ad4antr 745	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ≠ 𝑣)
74		simp-6r 800	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ≠ 𝑤)
75		simp-5r 798	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑢 ∈ (𝑣𝐿𝑤))
76		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡 ∈ 𝑃)
77	7	eqcomi 2771	. . . . . . . . . . . . . . 15 ⊢ (cgrA‘𝐺) = ∼
78	77	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (cgrA‘𝐺) = ∼ )
79		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ∈ (𝑋𝐼𝑡))
80		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ∈ (𝑢𝐼𝑤))
81		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝑌 − 𝑡) = (𝑣 − 𝑢))
82	81	eqcomd 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝑣 − 𝑢) = (𝑌 − 𝑡))
83	73	necomd 3012	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑣 ≠ 𝑢)
84	3, 6, 5, 61, 69, 67, 65, 76, 82, 83	tgcgrneq 28825	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑌 ≠ 𝑡)
85	84	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑡 ≠ 𝑌)
86	74	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → 𝑤 ≠ 𝑣)
87	3, 5, 6, 61, 63, 65, 76, 67, 69, 70, 79, 80, 71, 85, 73, 86	flatcgra 29212	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → ⟨“𝑋𝑌𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑤”⟩)
88	78, 87	breqdi 5122	. . . . . . . . . . . . 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 29269	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
90	59, 89	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑋𝑌𝑡”⟩)
91	90, 88	eqbrtrd 5131	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑌 ∈ (𝑋𝐼𝑡)) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
92	91	anasss 472	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑌 ∈ (𝑋𝐼𝑡) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
93	3, 6, 5, 60, 62, 64, 68, 66	axtgsegcon 28806	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → ∃𝑡 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑡) ∧ (𝑌 − 𝑡) = (𝑣 − 𝑢)))
94	92, 93	r19.29a 3172	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑣 ∈ (𝑢𝐼𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
95		simpr 490	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑢 ∈ (𝑣𝐿𝑤))
96		simplr 781	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ≠ 𝑤)
97	3, 5, 8, 10, 19, 21, 23, 31, 95, 96	lnrot2 28972	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ∈ (𝑢𝐿𝑣))
98	3, 5, 37, 19, 21, 23, 10, 13, 8, 97	lnhl 28961	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝑤((hlG‘𝐺)‘𝑣)𝑢 ∨ 𝑣 ∈ (𝑢𝐼𝑤)))
99	57, 94, 98	mpjaodan 973	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
100		simp-7r 802	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
101	100	oveq1d 7431	. . . . . . . . . . 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 28950	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑤((hlG‘𝐺)‘𝑣)𝑡)
122	3, 5, 37, 105, 105, 107, 103, 113	hlid 28955	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑋((hlG‘𝐺)‘𝑌)𝑋)
123	3, 7, 37, 103, 121, 122, 110, 107	zerocgra 29211	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑤𝑣𝑡”⟩ ∼ ⟨“𝑋𝑌𝑋”⟩)
124		simpr 490	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝑣 − 𝑡) = (𝑌 − 𝑋))
125	3, 5, 37, 112, 119, 110, 103, 8, 121	hlln 28953	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑤 ∈ (𝑡𝐿𝑣))
126	3, 8, 5, 103, 119, 110, 125	tglngne 28893	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ≠ 𝑣)
127	3, 5, 8, 103, 110, 112, 119, 117, 125, 126	lnrot1 28971	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ (𝑣𝐿𝑤))
128	3, 6, 5, 103, 119, 108	tgbtwntriv1 28834	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ (𝑡𝐼𝑢))
129	127, 128	elind 4149	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑡 ∈ ((𝑣𝐿𝑤) ∩ (𝑡𝐼𝑢)))
130	129	ne0d 4291	. . . . . . . . . . . 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 29268	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (⟨“𝑢𝑣𝑤”⟩ + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑢𝑣𝑡”⟩)
132	101, 131	eqtrd 2797	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) = ⟨“𝑢𝑣𝑡”⟩)
133	77	a1i 11	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (cgrA‘𝐺) = ∼ )
134	126	necomd 3012	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → 𝑣 ≠ 𝑡)
135	3, 5, 103, 37, 108, 110, 119, 116, 134	cgraid 29206	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑡”⟩)
136	3, 5, 37, 103, 108, 110, 119, 108, 110, 119, 135, 112, 121	cgrahl2 29204	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩(cgrA‘𝐺)⟨“𝑢𝑣𝑤”⟩)
137	133, 136	breqdi 5122	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → ⟨“𝑢𝑣𝑡”⟩ ∼ ⟨“𝑢𝑣𝑤”⟩)
138	132, 137	eqbrtrd 5131	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ 𝑡((hlG‘𝐺)‘𝑣)𝑤) ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
139	138	anasss 472	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡((hlG‘𝐺)‘𝑣)𝑤 ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
140		simplr 781	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑣 ≠ 𝑤)
141	140	necomd 3012	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → 𝑤 ≠ 𝑣)
142	3, 5, 37, 109, 106, 104, 102, 111, 6, 141, 114	hlcgrex 28962	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → ∃𝑡 ∈ 𝑃 (𝑡((hlG‘𝐺)‘𝑣)𝑤 ∧ (𝑣 − 𝑡) = (𝑌 − 𝑋)))
143	139, 142	r19.29a 3172	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) ∧ ¬ 𝑢 ∈ (𝑣𝐿𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
144	99, 143	pm2.61dan 825	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ ⟨“𝑢𝑣𝑤”⟩)
145		simpllr 788	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → 𝐸 = ⟨“𝑢𝑣𝑤”⟩)
146	144, 145	breqtrrd 5137	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ 𝑢 ≠ 𝑣) ∧ 𝑣 ≠ 𝑤) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
147	146	anasss 472	. . . 4 ⊢ ((((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ 𝐸 = ⟨“𝑢𝑣𝑤”⟩) ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤)) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
148	147	anasss 472	. . 3 ⊢ (((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ 𝑤 ∈ 𝑃) ∧ (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
149	148	r19.29an 3168	. 2 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑃) ∧ 𝑣 ∈ 𝑃) ∧ ∃𝑤 ∈ 𝑃 (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤))) → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)
150	3	fvexi 6896	. . 3 ⊢ 𝑃 ∈ V
151		angmgmaddlid.e	. . 3 ⊢ (𝜑 → 𝐸 ∈ 𝐴)
152	150, 4, 151	elcgrabasi 29255	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 ∃𝑤 ∈ 𝑃 (𝐸 = ⟨“𝑢𝑣𝑤”⟩ ∧ (𝑢 ≠ 𝑣 ∧ 𝑣 ≠ 𝑤)))
153	149, 152	r19.29vva 3224	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 2957 ∃wrex 3088 {crab 3414 ∖ cdif 3899 ∩ cin 3901 ∅c0 4282 ifcif 4485 {csn 4587 class class class wbr 5107 ‘cfv 6537 ℩crio 7372 (class class class)co 7416 ∈ cmpo 7418 ↑_m cmap 8829 0cc0 11127 1c1 11128 2c2 12322 3c3 12323 ..^cfzo 13711 ⟨“cs3 14915 Basecbs 17305 distcds 17355 TarskiGcstrkg 28769 Itvcitv 28775 LineGclng 28776 hlGchlg 28943 cgrAccgra 29194

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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-oadd 8462 df-er 8699 df-map 8831 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-xnn0 12605 df-z 12619 df-uz 12891 df-fz 13564 df-fzo 13712 df-hash 14397 df-word 14581 df-concat 14638 df-s1 14665 df-s2 14921 df-s3 14922 df-trkgc 28790 df-trkgb 28791 df-trkgcb 28792 df-trkgld 28794 df-trkg 28795 df-cgrg 28854 df-ismt 28876 df-leg 28926 df-hlg 28944 df-mir 29005 df-rag 29049 df-perpg 29051 df-hpg 29116 df-mid 29159 df-lmi 29160 df-cgra 29195

This theorem is used by: angmgmlem 29275

W3C validator