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

Theorem trgcopy 25816
 Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.)
Hypotheses
Ref Expression
trgcopy.p 𝑃 = (Base‘𝐺)
trgcopy.m = (dist‘𝐺)
trgcopy.i 𝐼 = (Itv‘𝐺)
trgcopy.l 𝐿 = (LineG‘𝐺)
trgcopy.k 𝐾 = (hlG‘𝐺)
trgcopy.g (𝜑𝐺 ∈ TarskiG)
trgcopy.a (𝜑𝐴𝑃)
trgcopy.b (𝜑𝐵𝑃)
trgcopy.c (𝜑𝐶𝑃)
trgcopy.d (𝜑𝐷𝑃)
trgcopy.e (𝜑𝐸𝑃)
trgcopy.f (𝜑𝐹𝑃)
trgcopy.1 (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
trgcopy.2 (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
trgcopy.3 (𝜑 → (𝐴 𝐵) = (𝐷 𝐸))
Assertion
Ref Expression
trgcopy (𝜑 → ∃𝑓𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
Distinct variable groups:   ,𝑓   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝐷,𝑓   𝑓,𝐸   𝑓,𝐹   𝑓,𝐺   𝑓,𝐼   𝑓,𝐿   𝑃,𝑓   𝜑,𝑓   𝑓,𝐾

Proof of Theorem trgcopy
Dummy variables 𝑗 𝑘 𝑙 𝑞 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 trgcopy.p . . . . . . 7 𝑃 = (Base‘𝐺)
2 trgcopy.m . . . . . . 7 = (dist‘𝐺)
3 eqid 2724 . . . . . . 7 (cgrG‘𝐺) = (cgrG‘𝐺)
4 trgcopy.g . . . . . . . . . . 11 (𝜑𝐺 ∈ TarskiG)
54ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
65ad2antrr 764 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
76ad2antrr 764 . . . . . . . 8 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG)
87adantr 472 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐺 ∈ TarskiG)
9 trgcopy.a . . . . . . . . . 10 (𝜑𝐴𝑃)
109ad2antrr 764 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴𝑃)
1110ad2antrr 764 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴𝑃)
1211ad3antrrr 768 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐴𝑃)
13 trgcopy.b . . . . . . . . . 10 (𝜑𝐵𝑃)
1413ad2antrr 764 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵𝑃)
1514ad2antrr 764 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵𝑃)
1615ad3antrrr 768 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐵𝑃)
17 trgcopy.c . . . . . . . . 9 (𝜑𝐶𝑃)
1817ad6antr 779 . . . . . . . 8 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶𝑃)
1918adantr 472 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐶𝑃)
20 trgcopy.d . . . . . . . . . 10 (𝜑𝐷𝑃)
2120ad2antrr 764 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷𝑃)
2221ad2antrr 764 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷𝑃)
2322ad3antrrr 768 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐷𝑃)
24 trgcopy.e . . . . . . . . . 10 (𝜑𝐸𝑃)
2524ad2antrr 764 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸𝑃)
2625ad2antrr 764 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸𝑃)
2726ad3antrrr 768 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐸𝑃)
28 simprl 811 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓𝑃)
29 trgcopy.3 . . . . . . . . 9 (𝜑 → (𝐴 𝐵) = (𝐷 𝐸))
3029ad2antrr 764 . . . . . . . 8 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 𝐵) = (𝐷 𝐸))
3130ad5antr 775 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐴 𝐵) = (𝐷 𝐸))
32 trgcopy.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
33 trgcopy.l . . . . . . . . . . 11 𝐿 = (LineG‘𝐺)
34 trgcopy.1 . . . . . . . . . . 11 (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
351, 33, 32, 4, 13, 17, 9, 34ncoltgdim2 25580 . . . . . . . . . 10 (𝜑𝐺DimTarskiG≥2)
3635ad4antr 771 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺DimTarskiG≥2)
3736ad3antrrr 768 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐺DimTarskiG≥2)
381, 32, 33, 4, 9, 13, 17, 34ncolne1 25640 . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
391, 32, 33, 4, 9, 13, 38tgelrnln 25645 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
4039ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
41 simplr 809 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵))
421, 33, 32, 5, 40, 41tglnpt 25564 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥𝑃)
4342ad2antrr 764 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑥𝑃)
4443ad2antrr 764 . . . . . . . . 9 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥𝑃)
4544adantr 472 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑥𝑃)
46 simplr 809 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦𝑃)
4746ad2antrr 764 . . . . . . . . 9 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦𝑃)
4847adantr 472 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦𝑃)
4941ad5antr 775 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵))
5038ad7antr 783 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐴𝐵)
511, 32, 33, 8, 12, 16, 50tglinecom 25650 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
5249, 51eleqtrd 2805 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴))
53 simp-6r 835 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
5433, 8, 53perpln1 25725 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
5540ad5antr 775 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿)
561, 2, 32, 33, 8, 54, 55, 53perpcom 25728 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥))
571, 33, 32, 4, 13, 17, 9, 34ncolrot2 25578 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
58 ioran 512 . . . . . . . . . . . . . . . . . 18 (¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
5957, 58sylib 208 . . . . . . . . . . . . . . . . 17 (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
6059simpld 477 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
6160ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
62 nelne2 2993 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥𝐶)
6341, 61, 62syl2anc 696 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥𝐶)
6463ad4antr 771 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥𝐶)
6564adantr 472 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑥𝐶)
6665necomd 2951 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐶𝑥)
671, 32, 33, 8, 19, 45, 66tglinecom 25650 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶))
6856, 51, 673brtr3d 4791 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶))
691, 2, 32, 33, 8, 16, 12, 52, 19, 68perprag 25738 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐵𝑥𝐶”⟩ ∈ (∟G‘𝐺))
701, 2, 32, 4, 9, 13, 20, 24, 29, 38tgcgrneq 25498 . . . . . . . . . . . 12 (𝜑𝐷𝐸)
7170necomd 2951 . . . . . . . . . . 11 (𝜑𝐸𝐷)
7271ad7antr 783 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐸𝐷)
7370ad4antr 771 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷𝐸)
7473neneqd 2901 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐷 = 𝐸)
7541orcd 406 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
761, 33, 32, 5, 10, 14, 42, 75colrot2 25575 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴))
771, 33, 32, 5, 42, 10, 14, 76colcom 25573 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
7877ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
79 simpr 479 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
801, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 78, 79lnxfr 25581 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦))
811, 33, 32, 6, 22, 46, 26, 80colrot2 25575 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
821, 33, 32, 6, 26, 22, 46, 81colcom 25573 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
8382orcomd 402 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷 = 𝐸𝑦 ∈ (𝐷𝐿𝐸)))
8483ord 391 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (¬ 𝐷 = 𝐸𝑦 ∈ (𝐷𝐿𝐸)))
8574, 84mpd 15 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ (𝐷𝐿𝐸))
8685ad3antrrr 768 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸))
871, 32, 33, 8, 27, 23, 48, 72, 86lncom 25637 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷))
88 simprrr 824 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦 𝑓) = (𝑥 𝐶))
8988eqcomd 2730 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑥 𝐶) = (𝑦 𝑓))
901, 2, 32, 8, 45, 19, 48, 28, 89, 65tgcgrneq 25498 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦𝑓)
911, 32, 33, 8, 48, 28, 90tgelrnln 25645 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿)
921, 32, 33, 8, 27, 23, 72tgelrnln 25645 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐸𝐿𝐷) ∈ ran 𝐿)
93 simpllr 817 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑞𝑃)
94 simplr 809 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞𝑃)
95 simprl 811 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦))
9633, 7, 95perpln2 25726 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿)
971, 32, 33, 7, 94, 47, 96tglnne 25643 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞𝑦)
9897adantr 472 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑞𝑦)
9998necomd 2951 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦𝑞)
1001, 32, 33, 8, 48, 93, 99tgelrnln 25645 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦𝐿𝑞) ∈ ran 𝐿)
10195adantr 472 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦))
1021, 32, 33, 8, 27, 23, 72tglinecom 25650 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸))
1031, 32, 33, 8, 48, 93, 100tglnne 25643 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑦𝑞)
1041, 32, 33, 8, 48, 93, 103tglinecom 25650 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦))
105101, 102, 1043brtr4d 4792 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞))
1061, 2, 32, 33, 8, 92, 100, 105perpcom 25728 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦𝐿𝑞)(⟂G‘𝐺)(𝐸𝐿𝐷))
107 trgcopy.k . . . . . . . . . . . . . 14 𝐾 = (hlG‘𝐺)
108 simprrl 823 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓(𝐾𝑦)𝑞)
1091, 32, 107, 28, 93, 48, 8, 33, 108hlln 25622 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦))
1101, 32, 33, 8, 48, 93, 28, 99, 109lncom 25637 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞))
111110orcd 406 . . . . . . . . . . 11 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞))
1121, 2, 32, 33, 8, 48, 93, 28, 106, 111, 90colperp 25741 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷))
1131, 2, 32, 33, 8, 91, 92, 112perpcom 25728 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓))
1141, 2, 32, 33, 8, 27, 23, 87, 28, 113perprag 25738 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐸𝑦𝑓”⟩ ∈ (∟G‘𝐺))
11579ad3antrrr 768 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
1161, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115cgr3simp2 25536 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐵 𝑥) = (𝐸 𝑦))
1171, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 114, 116, 89hypcgr 25813 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐵 𝐶) = (𝐸 𝑓))
118 eqid 2724 . . . . . . . . 9 (pInvG‘𝐺) = (pInvG‘𝐺)
11951, 68eqbrtrd 4782 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶))
1201, 2, 32, 33, 8, 12, 16, 49, 19, 119perprag 25738 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐴𝑥𝐶”⟩ ∈ (∟G‘𝐺))
1211, 2, 32, 33, 118, 8, 12, 45, 19, 120ragcom 25713 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐶𝑥𝐴”⟩ ∈ (∟G‘𝐺))
122102, 113eqbrtrrd 4784 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓))
1231, 2, 32, 33, 8, 23, 27, 86, 28, 122perprag 25738 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐷𝑦𝑓”⟩ ∈ (∟G‘𝐺))
1241, 2, 32, 33, 118, 8, 23, 48, 28, 123ragcom 25713 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝑓𝑦𝐷”⟩ ∈ (∟G‘𝐺))
1251, 2, 32, 8, 45, 19, 48, 28, 89tgcgrcomlr 25495 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐶 𝑥) = (𝑓 𝑦))
1261, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115cgr3simp3 25537 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑥 𝐴) = (𝑦 𝐷))
1271, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 121, 124, 125, 126hypcgr 25813 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐶 𝐴) = (𝑓 𝐷))
1281, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 117, 127trgcgr 25531 . . . . . 6 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
1291, 32, 33, 4, 20, 24, 70tgelrnln 25645 . . . . . . . . 9 (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
130129ad4antr 771 . . . . . . . 8 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷𝐿𝐸) ∈ ran 𝐿)
131130ad3antrrr 768 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
132 simpl 474 . . . . . . . . . . 11 ((𝑤 = 𝑘𝑣 = 𝑙) → 𝑤 = 𝑘)
133 eqidd 2725 . . . . . . . . . . 11 ((𝑤 = 𝑘𝑣 = 𝑙) → (𝑃 ∖ (𝐷𝐿𝐸)) = (𝑃 ∖ (𝐷𝐿𝐸)))
134132, 133eleq12d 2797 . . . . . . . . . 10 ((𝑤 = 𝑘𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
135 simpr 479 . . . . . . . . . . 11 ((𝑤 = 𝑘𝑣 = 𝑙) → 𝑣 = 𝑙)
136135, 133eleq12d 2797 . . . . . . . . . 10 ((𝑤 = 𝑘𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
137134, 136anbi12d 749 . . . . . . . . 9 ((𝑤 = 𝑘𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))))
138 simpr 479 . . . . . . . . . . 11 (((𝑤 = 𝑘𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗)
139 simpll 807 . . . . . . . . . . . 12 (((𝑤 = 𝑘𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘)
140 simplr 809 . . . . . . . . . . . 12 (((𝑤 = 𝑘𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙)
141139, 140oveq12d 6783 . . . . . . . . . . 11 (((𝑤 = 𝑘𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙))
142138, 141eleq12d 2797 . . . . . . . . . 10 (((𝑤 = 𝑘𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙)))
143142cbvrexdva 3281 . . . . . . . . 9 ((𝑤 = 𝑘𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))
144137, 143anbi12d 749 . . . . . . . 8 ((𝑤 = 𝑘𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))))
145144cbvopabv 4830 . . . . . . 7 {⟨𝑤, 𝑣⟩ ∣ ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣))} = {⟨𝑘, 𝑙⟩ ∣ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))}
1468adantr 472 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG)
14719adantr 472 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐶𝑃)
14816adantr 472 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐵𝑃)
14912adantr 472 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐴𝑃)
15023adantr 472 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐷𝑃)
15127adantr 472 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸𝑃)
15228adantr 472 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓𝑃)
15371ad8antr 787 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸𝐷)
154 simpr 479 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸))
1551, 32, 33, 146, 151, 150, 152, 153, 154lncom 25637 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷))
156155orcd 406 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
1571, 33, 32, 146, 151, 150, 152, 156colrot1 25574 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐸 ∈ (𝐷𝐿𝑓) ∨ 𝐷 = 𝑓))
158128adantr 472 . . . . . . . . . . . . . 14 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
1591, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158trgcgrcom 25543 . . . . . . . . . . . . 13 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐷𝐸𝑓”⟩(cgrG‘𝐺)⟨“𝐴𝐵𝐶”⟩)
1601, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159lnxfr 25581 . . . . . . . . . . . 12 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
1611, 33, 32, 146, 149, 147, 148, 160colrot1 25574 . . . . . . . . . . 11 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
1621, 33, 32, 146, 147, 148, 149, 161colcom 25573 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
16334ad8antr 787 . . . . . . . . . 10 (((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
164162, 163pm2.65da 601 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → ¬ 𝑓 ∈ (𝐷𝐿𝐸))
165108, 164jca 555 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑓(𝐾𝑦)𝑞 ∧ ¬ 𝑓 ∈ (𝐷𝐿𝐸)))
166109orcd 406 . . . . . . . . . 10 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑓 ∈ (𝑞𝐿𝑦) ∨ 𝑞 = 𝑦))
1671, 33, 32, 8, 93, 48, 28, 166colrot2 25575 . . . . . . . . 9 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑦 ∈ (𝑓𝐿𝑞) ∨ 𝑓 = 𝑞))
1681, 32, 33, 8, 131, 28, 145, 93, 86, 167, 107colhp 25782 . . . . . . . 8 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞 ↔ (𝑓(𝐾𝑦)𝑞 ∧ ¬ 𝑓 ∈ (𝐷𝐿𝐸))))
169165, 168mpbird 247 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞)
170 trgcopy.f . . . . . . . . . 10 (𝜑𝐹𝑃)
171170ad4antr 771 . . . . . . . . 9 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹𝑃)
172171ad2antrr 764 . . . . . . . 8 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐹𝑃)
173172adantr 472 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝐹𝑃)
174 simplrr 820 . . . . . . 7 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
1751, 32, 33, 8, 131, 28, 145, 93, 169, 173, 174hpgtr 25780 . . . . . 6 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
176128, 175jca 555 . . . . 5 ((((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓𝑃 ∧ (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))) → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
1771, 32, 107, 47, 44, 18, 7, 94, 2, 97, 64hlcgrex 25631 . . . . 5 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓𝑃 (𝑓(𝐾𝑦)𝑞 ∧ (𝑦 𝑓) = (𝑥 𝐶)))
178176, 177reximddv 3120 . . . 4 (((((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
179 trgcopy.2 . . . . . . . . 9 (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
1801, 33, 32, 4, 24, 170, 20, 179ncolrot2 25578 . . . . . . . 8 (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
181 ioran 512 . . . . . . . 8 (¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
182180, 181sylib 208 . . . . . . 7 (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
183182simpld 477 . . . . . 6 (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
184183ad4antr 771 . . . . 5 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
1851, 2, 32, 33, 6, 36, 130, 145, 85, 171, 184lnperpex 25815 . . . 4 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑞𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
186178, 185r19.29a 3180 . . 3 (((((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑓𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
1871, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 77, 30lnext 25582 . . 3 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦𝑃 ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
188186, 187r19.29a 3180 . 2 (((𝜑𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
1891, 2, 32, 33, 4, 39, 17, 60footex 25733 . 2 (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
190188, 189r19.29a 3180 1 (𝜑 → ∃𝑓𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1596   ∈ wcel 2103   ≠ wne 2896  ∃wrex 3015   ∖ cdif 3677   class class class wbr 4760  {copab 4820  ran crn 5219  ‘cfv 6001  (class class class)co 6765  2c2 11183  ⟨“cs3 13708  Basecbs 15980  distcds 16073  TarskiGcstrkg 25449  DimTarskiG≥cstrkgld 25453  Itvcitv 25455  LineGclng 25456  cgrGccgrg 25525  hlGchlg 25615  pInvGcmir 25667  ⟂Gcperpg 25710  hpGchpg 25769 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-pm 7977  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-2 11192  df-3 11193  df-n0 11406  df-xnn0 11477  df-z 11491  df-uz 11801  df-fz 12441  df-fzo 12581  df-hash 13233  df-word 13406  df-concat 13408  df-s1 13409  df-s2 13714  df-s3 13715  df-trkgc 25467  df-trkgb 25468  df-trkgcb 25469  df-trkgld 25471  df-trkg 25472  df-cgrg 25526  df-ismt 25548  df-leg 25598  df-hlg 25616  df-mir 25668  df-rag 25709  df-perpg 25711  df-hpg 25770  df-mid 25786  df-lmi 25787 This theorem is referenced by:  trgcopyeu  25818  acopy  25844  cgrg3col4  25854
 Copyright terms: Public domain W3C validator