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

Theorem trgcopyeulem 28045
Description: Lemma for trgcopyeu 28046. (Contributed by Thierry Arnoux, 8-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 (πœ‘ β†’ (𝐴 βˆ’ 𝐡) = (𝐷 βˆ’ 𝐸))
trgcopyeulem.o 𝑂 = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 βˆ– (𝐷𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 βˆ– (𝐷𝐿𝐸))) ∧ βˆƒπ‘‘ ∈ (𝐷𝐿𝐸)𝑑 ∈ (π‘ŽπΌπ‘))}
trgcopyeulem.x (πœ‘ β†’ 𝑋 ∈ 𝑃)
trgcopyeulem.y (πœ‘ β†’ π‘Œ ∈ 𝑃)
trgcopyeulem.1 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ·πΈπ‘‹β€βŸ©)
trgcopyeulem.2 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ·πΈπ‘Œβ€βŸ©)
trgcopyeulem.3 (πœ‘ β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
trgcopyeulem.4 (πœ‘ β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
Assertion
Ref Expression
trgcopyeulem (πœ‘ β†’ 𝑋 = π‘Œ)
Distinct variable groups:   βˆ’ ,π‘Ž,𝑏,𝑑   𝐴,π‘Ž,𝑏,𝑑   𝐡,π‘Ž,𝑏,𝑑   𝐢,π‘Ž,𝑏,𝑑   𝐷,π‘Ž,𝑏,𝑑   𝐸,π‘Ž,𝑏,𝑑   𝐹,π‘Ž,𝑏,𝑑   𝐺,π‘Ž,𝑏,𝑑   𝐼,π‘Ž,𝑏,𝑑   𝐿,π‘Ž,𝑏,𝑑   𝑃,π‘Ž,𝑏,𝑑   πœ‘,π‘Ž,𝑏,𝑑   𝐾,π‘Ž   𝑂,π‘Ž,𝑏,𝑑   𝑋,π‘Ž,𝑏,𝑑   π‘Œ,π‘Ž,𝑏,𝑑
Allowed substitution hints:   𝐾(𝑑,𝑏)

Proof of Theorem trgcopyeulem
StepHypRef Expression
1 trgcopy.p . 2 𝑃 = (Baseβ€˜πΊ)
2 trgcopy.m . 2 βˆ’ = (distβ€˜πΊ)
3 trgcopy.i . 2 𝐼 = (Itvβ€˜πΊ)
4 trgcopy.g . 2 (πœ‘ β†’ 𝐺 ∈ TarskiG)
5 trgcopy.l . . 3 𝐿 = (LineGβ€˜πΊ)
6 trgcopy.b . . 3 (πœ‘ β†’ 𝐡 ∈ 𝑃)
7 trgcopy.c . . 3 (πœ‘ β†’ 𝐢 ∈ 𝑃)
8 trgcopy.a . . 3 (πœ‘ β†’ 𝐴 ∈ 𝑃)
9 trgcopy.1 . . 3 (πœ‘ β†’ Β¬ (𝐴 ∈ (𝐡𝐿𝐢) ∨ 𝐡 = 𝐢))
101, 5, 3, 4, 6, 7, 8, 9ncoltgdim2 27805 . 2 (πœ‘ β†’ 𝐺DimTarskiGβ‰₯2)
11 eqid 2732 . 2 ((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸)) = ((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))
12 trgcopy.d . . 3 (πœ‘ β†’ 𝐷 ∈ 𝑃)
13 trgcopy.e . . 3 (πœ‘ β†’ 𝐸 ∈ 𝑃)
14 trgcopy.f . . . 4 (πœ‘ β†’ 𝐹 ∈ 𝑃)
15 trgcopy.2 . . . 4 (πœ‘ β†’ Β¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
161, 3, 5, 4, 12, 13, 14, 15ncolne1 27865 . . 3 (πœ‘ β†’ 𝐷 β‰  𝐸)
171, 3, 5, 4, 12, 13, 16tgelrnln 27870 . 2 (πœ‘ β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
18 trgcopyeulem.x . 2 (πœ‘ β†’ 𝑋 ∈ 𝑃)
19 trgcopyeulem.y . 2 (πœ‘ β†’ π‘Œ ∈ 𝑃)
20 eqid 2732 . . . . . . . . 9 (pInvGβ€˜πΊ) = (pInvGβ€˜πΊ)
214ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐺 ∈ TarskiG)
2217ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
23 simplr 767 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ (𝐷𝐿𝐸))
241, 5, 3, 21, 22, 23tglnpt 27789 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ 𝑃)
25 eqid 2732 . . . . . . . . 9 ((pInvGβ€˜πΊ)β€˜π‘‘) = ((pInvGβ€˜πΊ)β€˜π‘‘)
261, 2, 3, 4, 10, 11, 5, 17, 19lmicl 28026 . . . . . . . . . 10 (πœ‘ β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ∈ 𝑃)
2726ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ∈ 𝑃)
2818ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑋 ∈ 𝑃)
2912ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐷 ∈ 𝑃)
3013ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐸 ∈ 𝑃)
31 eqid 2732 . . . . . . . . . . . 12 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
3216ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐷 β‰  𝐸)
3332necomd 2996 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐸 β‰  𝐷)
341, 3, 5, 21, 30, 29, 24, 33, 23lncom 27862 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ (𝐸𝐿𝐷))
3534orcd 871 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝑑 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
361, 5, 3, 21, 30, 29, 24, 35colrot1 27799 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐸 ∈ (𝐷𝐿𝑑) ∨ 𝐷 = 𝑑))
37 trgcopyeulem.1 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ·πΈπ‘‹β€βŸ©)
381, 2, 3, 31, 4, 8, 6, 7, 12, 13, 18, 37cgr3simp3 27762 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = (𝑋 βˆ’ 𝐷))
391, 2, 3, 4, 7, 8, 18, 12, 38tgcgrcomlr 27720 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴 βˆ’ 𝐢) = (𝐷 βˆ’ 𝑋))
40 trgcopyeulem.2 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ·πΈπ‘Œβ€βŸ©)
411, 2, 3, 31, 4, 8, 6, 7, 12, 13, 19, 40cgr3simp3 27762 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = (π‘Œ βˆ’ 𝐷))
421, 2, 3, 4, 7, 8, 19, 12, 41tgcgrcomlr 27720 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴 βˆ’ 𝐢) = (𝐷 βˆ’ π‘Œ))
4339, 42eqtr3d 2774 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ π‘Œ))
441, 2, 3, 4, 10, 11, 5, 17, 12, 19lmiiso 28037 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π·) βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐷 βˆ’ π‘Œ))
451, 3, 5, 4, 12, 13, 16tglinerflx1 27873 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐷 ∈ (𝐷𝐿𝐸))
461, 2, 3, 4, 10, 11, 5, 17, 12, 45lmicinv 28033 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π·) = 𝐷)
4746oveq1d 7420 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π·) βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐷 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
4843, 44, 473eqtr2d 2778 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
4948ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
501, 2, 3, 31, 4, 8, 6, 7, 12, 13, 18, 37cgr3simp2 27761 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐸 βˆ’ 𝑋))
511, 2, 3, 31, 4, 8, 6, 7, 12, 13, 19, 40cgr3simp2 27761 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐸 βˆ’ π‘Œ))
5250, 51eqtr3d 2774 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ π‘Œ))
531, 2, 3, 4, 10, 11, 5, 17, 13, 19lmiiso 28037 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜πΈ) βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐸 βˆ’ π‘Œ))
541, 3, 5, 4, 12, 13, 16tglinerflx2 27874 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐸 ∈ (𝐷𝐿𝐸))
551, 2, 3, 4, 10, 11, 5, 17, 13, 54lmicinv 28033 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜πΈ) = 𝐸)
5655oveq1d 7420 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜πΈ) βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐸 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
5752, 53, 563eqtr2d 2778 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
5857ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
591, 5, 3, 21, 29, 30, 24, 31, 28, 27, 2, 32, 36, 49, 58lncgr 27809 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝑑 βˆ’ 𝑋) = (𝑑 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
60 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
611, 2, 3, 5, 20, 21, 24, 25, 27, 28, 59, 60ismir 27899 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑋 = (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
6261eqcomd 2738 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = 𝑋)
631, 2, 3, 5, 20, 21, 24, 25, 27, 62mircom 27903 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹) = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
6463eqcomd 2738 . . . . . . 7 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) = (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹))
6510ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝐺DimTarskiGβ‰₯2)
661, 2, 3, 21, 65, 28, 27, 20, 24ismidb 28018 . . . . . . 7 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) = (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹) ↔ (𝑋(midGβ€˜πΊ)(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = 𝑑))
6764, 66mpbid 231 . . . . . 6 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝑋(midGβ€˜πΊ)(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = 𝑑)
6867, 23eqeltrd 2833 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝑋(midGβ€˜πΊ)(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ (𝐷𝐿𝐸))
69 trgcopyeulem.o . . . . . . . . 9 𝑂 = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 βˆ– (𝐷𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 βˆ– (𝐷𝐿𝐸))) ∧ βˆƒπ‘‘ ∈ (𝐷𝐿𝐸)𝑑 ∈ (π‘ŽπΌπ‘))}
70 trgcopyeulem.4 . . . . . . . . 9 (πœ‘ β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
71 trgcopyeulem.3 . . . . . . . . . 10 (πœ‘ β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
721, 3, 5, 4, 17, 18, 69, 14, 71hpgcom 28007 . . . . . . . . 9 (πœ‘ β†’ 𝐹((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝑋)
731, 3, 5, 4, 17, 19, 69, 14, 70, 18, 72hpgtr 28008 . . . . . . . 8 (πœ‘ β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝑋)
741, 3, 5, 69, 4, 17, 19, 14, 70hpgne1 28001 . . . . . . . . . 10 (πœ‘ β†’ Β¬ π‘Œ ∈ (𝐷𝐿𝐸))
751, 2, 3, 5, 4, 10, 17, 69, 11, 19, 74lmiopp 28042 . . . . . . . . 9 (πœ‘ β†’ π‘Œπ‘‚(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
761, 3, 5, 69, 4, 17, 19, 18, 26, 75lnopp2hpgb 28003 . . . . . . . 8 (πœ‘ β†’ (𝑋𝑂(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ↔ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝑋))
7773, 76mpbird 256 . . . . . . 7 (πœ‘ β†’ 𝑋𝑂(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
781, 2, 3, 69, 18, 26islnopp 27979 . . . . . . 7 (πœ‘ β†’ (𝑋𝑂(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ↔ ((Β¬ 𝑋 ∈ (𝐷𝐿𝐸) ∧ Β¬ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ∈ (𝐷𝐿𝐸)) ∧ βˆƒπ‘‘ ∈ (𝐷𝐿𝐸)𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))))
7977, 78mpbid 231 . . . . . 6 (πœ‘ β†’ ((Β¬ 𝑋 ∈ (𝐷𝐿𝐸) ∧ Β¬ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) ∈ (𝐷𝐿𝐸)) ∧ βˆƒπ‘‘ ∈ (𝐷𝐿𝐸)𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))))
8079simprd 496 . . . . 5 (πœ‘ β†’ βˆƒπ‘‘ ∈ (𝐷𝐿𝐸)𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
8168, 80r19.29a 3162 . . . 4 (πœ‘ β†’ (𝑋(midGβ€˜πΊ)(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ (𝐷𝐿𝐸))
8221adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝐺 ∈ TarskiG)
8322adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
841, 2, 3, 69, 5, 17, 4, 18, 26, 77oppne3 27983 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 β‰  (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
851, 3, 5, 4, 18, 26, 84tgelrnln 27870 . . . . . . . . . 10 (πœ‘ β†’ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ ran 𝐿)
8685ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ ran 𝐿)
8786adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ ran 𝐿)
8884ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑋 β‰  (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
891, 3, 5, 21, 28, 27, 24, 88, 60btwnlng1 27859 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
9023, 89elind 4193 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 ∈ ((𝐷𝐿𝐸) ∩ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))))
9190adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝑑 ∈ ((𝐷𝐿𝐸) ∩ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))))
9254ad3antrrr 728 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝐸 ∈ (𝐷𝐿𝐸))
931, 3, 5, 4, 18, 26, 84tglinerflx1 27873 . . . . . . . . 9 (πœ‘ β†’ 𝑋 ∈ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
9493ad3antrrr 728 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝑋 ∈ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
95 simpr 485 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝐸 β‰  𝑑)
9679simplld 766 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝑋 ∈ (𝐷𝐿𝐸))
9796ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ Β¬ 𝑋 ∈ (𝐷𝐿𝐸))
98 nelne2 3040 . . . . . . . . . . 11 ((𝑑 ∈ (𝐷𝐿𝐸) ∧ Β¬ 𝑋 ∈ (𝐷𝐿𝐸)) β†’ 𝑑 β‰  𝑋)
9923, 97, 98syl2anc 584 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑑 β‰  𝑋)
10099necomd 2996 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ 𝑋 β‰  𝑑)
101100adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝑋 β‰  𝑑)
10264oveq2d 7421 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐸 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐸 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
10358, 102eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
104103adantr 481 . . . . . . . . 9 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
10530adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝐸 ∈ 𝑃)
10624adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝑑 ∈ 𝑃)
10728adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ 𝑋 ∈ 𝑃)
1081, 2, 3, 5, 20, 82, 105, 106, 107israg 27937 . . . . . . . . 9 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ (βŸ¨β€œπΈπ‘‘π‘‹β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝐸 βˆ’ 𝑋) = (𝐸 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹))))
109104, 108mpbird 256 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ βŸ¨β€œπΈπ‘‘π‘‹β€βŸ© ∈ (∟Gβ€˜πΊ))
1101, 2, 3, 5, 82, 83, 87, 91, 92, 94, 95, 101, 109ragperp 27957 . . . . . . 7 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐸 β‰  𝑑) β†’ (𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
11121adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝐺 ∈ TarskiG)
11222adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
11386adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ ran 𝐿)
11490adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝑑 ∈ ((𝐷𝐿𝐸) ∩ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))))
11545ad3antrrr 728 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝐷 ∈ (𝐷𝐿𝐸))
11693ad3antrrr 728 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝑋 ∈ (𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
117 simpr 485 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝐷 β‰  𝑑)
118100adantr 481 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝑋 β‰  𝑑)
11964oveq2d 7421 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐷 βˆ’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) = (𝐷 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
12049, 119eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
121120adantr 481 . . . . . . . . 9 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹)))
12229adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝐷 ∈ 𝑃)
12324adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝑑 ∈ 𝑃)
12428adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ 𝑋 ∈ 𝑃)
1251, 2, 3, 5, 20, 111, 122, 123, 124israg 27937 . . . . . . . . 9 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ (βŸ¨β€œπ·π‘‘π‘‹β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝐷 βˆ’ 𝑋) = (𝐷 βˆ’ (((pInvGβ€˜πΊ)β€˜π‘‘)β€˜π‘‹))))
126121, 125mpbird 256 . . . . . . . 8 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ βŸ¨β€œπ·π‘‘π‘‹β€βŸ© ∈ (∟Gβ€˜πΊ))
1271, 2, 3, 5, 111, 112, 113, 114, 115, 116, 117, 118, 126ragperp 27957 . . . . . . 7 ((((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) ∧ 𝐷 β‰  𝑑) β†’ (𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
128 neneor 3042 . . . . . . . 8 (𝐸 β‰  𝐷 β†’ (𝐸 β‰  𝑑 ∨ 𝐷 β‰  𝑑))
12933, 128syl 17 . . . . . . 7 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐸 β‰  𝑑 ∨ 𝐷 β‰  𝑑))
130110, 127, 129mpjaodan 957 . . . . . 6 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ (𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
131130orcd 871 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ (𝐷𝐿𝐸)) ∧ 𝑑 ∈ (𝑋𝐼(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))) β†’ ((𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∨ 𝑋 = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
132131, 80r19.29a 3162 . . . 4 (πœ‘ β†’ ((𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∨ 𝑋 = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))
1331, 2, 3, 4, 10, 11, 5, 17, 18, 26islmib 28027 . . . 4 (πœ‘ β†’ ((((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘‹) ↔ ((𝑋(midGβ€˜πΊ)(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∈ (𝐷𝐿𝐸) ∧ ((𝐷𝐿𝐸)(βŸ‚Gβ€˜πΊ)(𝑋𝐿(((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)) ∨ 𝑋 = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ)))))
13481, 132, 133mpbir2and 711 . . 3 (πœ‘ β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ) = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘‹))
135134eqcomd 2738 . 2 (πœ‘ β†’ (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘‹) = (((lInvGβ€˜πΊ)β€˜(𝐷𝐿𝐸))β€˜π‘Œ))
1361, 2, 3, 4, 10, 11, 5, 17, 18, 19, 135lmieq 28031 1 (πœ‘ β†’ 𝑋 = π‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆƒwrex 3070   βˆ– cdif 3944   ∩ cin 3946   class class class wbr 5147  {copab 5209  ran crn 5676  β€˜cfv 6540  (class class class)co 7405  2c2 12263  βŸ¨β€œcs3 14789  Basecbs 17140  distcds 17202  TarskiGcstrkg 27667  DimTarskiGβ‰₯cstrkgld 27671  Itvcitv 27673  LineGclng 27674  cgrGccgrg 27750  hlGchlg 27840  pInvGcmir 27892  βˆŸGcrag 27933  βŸ‚Gcperpg 27935  hpGchpg 27997  midGcmid 28012  lInvGclmi 28013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-xnn0 12541  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-hash 14287  df-word 14461  df-concat 14517  df-s1 14542  df-s2 14795  df-s3 14796  df-trkgc 27688  df-trkgb 27689  df-trkgcb 27690  df-trkgld 27692  df-trkg 27693  df-cgrg 27751  df-leg 27823  df-hlg 27841  df-mir 27893  df-rag 27934  df-perpg 27936  df-hpg 27998  df-mid 28014  df-lmi 28015
This theorem is referenced by:  trgcopyeu  28046  acopyeu  28074
  Copyright terms: Public domain W3C validator