Metamath Proof Explorer

Theorem trgcopyeulem

Description: Lemma for trgcopyeu . (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Hypotheses 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 trgcopyeulem ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 trgcopy.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 trgcopy.m ⊢ − = ( dist ‘ 𝐺 )
3 trgcopy.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 trgcopy.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 trgcopy.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 trgcopy.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 trgcopy.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 trgcopy.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 trgcopy.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 trgcopy.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 trgcopy.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
12 trgcopy.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
13 trgcopy.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
14 trgcopy.2 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
15 trgcopy.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
16 trgcopyeulem.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
17 trgcopyeulem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
18 trgcopyeulem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
19 trgcopyeulem.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
20 trgcopyeulem.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑌 ”⟩ )
21 trgcopyeulem.3 ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
22 trgcopyeulem.4 ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
23 1 4 3 6 8 9 7 13 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
24 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) )
25 1 3 4 6 10 11 12 14 ncolne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
26 1 3 4 6 10 11 25 tgelrnln ⊢ ( 𝜑 → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
27 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
28 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐺 ∈ TarskiG )
29 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
30 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) )
31 1 4 3 28 29 30 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ 𝑃 )
32 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 )
33 1 2 3 6 23 24 4 26 18 lmicl ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ∈ 𝑃 )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ∈ 𝑃 )
35 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑋 ∈ 𝑃 )
36 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐷 ∈ 𝑃 )
37 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐸 ∈ 𝑃 )
38 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
39 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐷 ≠ 𝐸 )
40 39 necomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐸 ≠ 𝐷 )
41 1 3 4 28 37 36 31 40 30 lncom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ ( 𝐸 𝐿 𝐷 ) )
42 41 orcd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝑡 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
43 1 4 3 28 37 36 31 42 colrot1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐸 ∈ ( 𝐷 𝐿 𝑡 ) ∨ 𝐷 = 𝑡 ) )
44 1 2 3 38 6 7 8 9 10 11 17 19 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝑋 − 𝐷 ) )
45 1 2 3 6 9 7 17 10 44 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝑋 ) )
46 1 2 3 38 6 7 8 9 10 11 18 20 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝑌 − 𝐷 ) )
47 1 2 3 6 9 7 18 10 46 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝑌 ) )
48 45 47 eqtr3d ⊢ ( 𝜑 → ( 𝐷 − 𝑋 ) = ( 𝐷 − 𝑌 ) )
49 1 2 3 6 23 24 4 26 10 18 lmiiso ⊢ ( 𝜑 → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐷 ) − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐷 − 𝑌 ) )
50 1 3 4 6 10 11 25 tglinerflx1 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐷 𝐿 𝐸 ) )
51 1 2 3 6 23 24 4 26 10 50 lmicinv ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐷 ) = 𝐷 )
52 51 oveq1d ⊢ ( 𝜑 → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐷 ) − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐷 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
53 48 49 52 3eqtr2d ⊢ ( 𝜑 → ( 𝐷 − 𝑋 ) = ( 𝐷 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐷 − 𝑋 ) = ( 𝐷 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
55 1 2 3 38 6 7 8 9 10 11 17 19 cgr3simp2 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑋 ) )
56 1 2 3 38 6 7 8 9 10 11 18 20 cgr3simp2 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑌 ) )
57 55 56 eqtr3d ⊢ ( 𝜑 → ( 𝐸 − 𝑋 ) = ( 𝐸 − 𝑌 ) )
58 1 2 3 6 23 24 4 26 11 18 lmiiso ⊢ ( 𝜑 → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐸 ) − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐸 − 𝑌 ) )
59 1 3 4 6 10 11 25 tglinerflx2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
60 1 2 3 6 23 24 4 26 11 59 lmicinv ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐸 ) = 𝐸 )
61 60 oveq1d ⊢ ( 𝜑 → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝐸 ) − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐸 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
62 57 58 61 3eqtr2d ⊢ ( 𝜑 → ( 𝐸 − 𝑋 ) = ( 𝐸 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐸 − 𝑋 ) = ( 𝐸 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
64 1 4 3 28 36 37 31 38 35 34 2 39 43 54 63 lncgr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝑡 − 𝑋 ) = ( 𝑡 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
65 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
66 1 2 3 4 27 28 31 32 34 35 64 65 ismir ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
67 66 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = 𝑋 )
68 1 2 3 4 27 28 31 32 34 67 mircom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
69 68 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) )
70 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝐺 DimTarskiG≥ 2 )
71 1 2 3 28 70 35 34 27 31 ismidb ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = 𝑡 ) )
72 69 71 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝑋 ( midG ‘ 𝐺 ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = 𝑡 )
73 72 30 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝑋 ( midG ‘ 𝐺 ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ( 𝐷 𝐿 𝐸 ) )
74 1 3 4 6 26 17 16 12 21 hpgcom ⊢ ( 𝜑 → 𝐹 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝑋 )
75 1 3 4 6 26 18 16 12 22 17 74 hpgtr ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝑋 )
76 1 3 4 16 6 26 18 12 22 hpgne1 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝐷 𝐿 𝐸 ) )
77 1 2 3 4 6 23 26 16 24 18 76 lmiopp ⊢ ( 𝜑 → 𝑌 𝑂 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
78 1 3 4 16 6 26 18 17 33 77 lnopp2hpgb ⊢ ( 𝜑 → ( 𝑋 𝑂 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ↔ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝑋 ) )
79 75 78 mpbird ⊢ ( 𝜑 → 𝑋 𝑂 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
80 1 2 3 16 17 33 islnopp ⊢ ( 𝜑 → ( 𝑋 𝑂 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ↔ ( ( ¬ 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ) )
81 79 80 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) )
82 81 simprd ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
83 73 82 r19.29a ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ( 𝐷 𝐿 𝐸 ) )
84 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝐺 ∈ TarskiG )
85 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
86 1 2 3 16 4 26 6 17 33 79 oppne3 ⊢ ( 𝜑 → 𝑋 ≠ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
87 1 3 4 6 17 33 86 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ran 𝐿 )
88 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ran 𝐿 )
89 88 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ran 𝐿 )
90 86 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑋 ≠ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
91 1 3 4 28 35 34 31 90 65 btwnlng1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
92 30 91 elind ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ∈ ( ( 𝐷 𝐿 𝐸 ) ∩ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) )
93 92 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝑡 ∈ ( ( 𝐷 𝐿 𝐸 ) ∩ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) )
94 59 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
95 1 3 4 6 17 33 86 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
96 95 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝑋 ∈ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
97 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝐸 ≠ 𝑡 )
98 81 simplld ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ¬ 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) )
100 nelne2 ⊢ ( ( 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑡 ≠ 𝑋 )
101 30 99 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑡 ≠ 𝑋 )
102 101 necomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → 𝑋 ≠ 𝑡 )
103 102 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝑋 ≠ 𝑡 )
104 69 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐸 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
105 63 104 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐸 − 𝑋 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
106 105 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ( 𝐸 − 𝑋 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
107 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝐸 ∈ 𝑃 )
108 31 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝑡 ∈ 𝑃 )
109 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → 𝑋 ∈ 𝑃 )
110 1 2 3 4 27 84 107 108 109 israg ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ( ⟨“ 𝐸 𝑡 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐸 − 𝑋 ) = ( 𝐸 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) ) )
111 106 110 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ⟨“ 𝐸 𝑡 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
112 1 2 3 4 84 85 89 93 94 96 97 103 111 ragperp ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐸 ≠ 𝑡 ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
113 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝐺 ∈ TarskiG )
114 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
115 88 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ran 𝐿 )
116 92 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝑡 ∈ ( ( 𝐷 𝐿 𝐸 ) ∩ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) )
117 50 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝐷 ∈ ( 𝐷 𝐿 𝐸 ) )
118 95 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝑋 ∈ ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
119 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝐷 ≠ 𝑡 )
120 102 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝑋 ≠ 𝑡 )
121 69 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐷 − ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) = ( 𝐷 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
122 54 121 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐷 − 𝑋 ) = ( 𝐷 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
123 122 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ( 𝐷 − 𝑋 ) = ( 𝐷 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) )
124 36 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝐷 ∈ 𝑃 )
125 31 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝑡 ∈ 𝑃 )
126 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → 𝑋 ∈ 𝑃 )
127 1 2 3 4 27 113 124 125 126 israg ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ( ⟨“ 𝐷 𝑡 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐷 − 𝑋 ) = ( 𝐷 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑡 ) ‘ 𝑋 ) ) ) )
128 123 127 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ⟨“ 𝐷 𝑡 𝑋 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
129 1 2 3 4 113 114 115 116 117 118 119 120 128 ragperp ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ∧ 𝐷 ≠ 𝑡 ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
130 neneor ⊢ ( 𝐸 ≠ 𝐷 → ( 𝐸 ≠ 𝑡 ∨ 𝐷 ≠ 𝑡 ) )
131 40 130 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐸 ≠ 𝑡 ∨ 𝐷 ≠ 𝑡 ) )
132 112 129 131 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
133 132 orcd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑡 ∈ ( 𝑋 𝐼 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) → ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∨ 𝑋 = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
134 133 82 r19.29a ⊢ ( 𝜑 → ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∨ 𝑋 = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) )
135 1 2 3 6 23 24 4 26 17 33 islmib ⊢ ( 𝜑 → ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑋 ) ↔ ( ( 𝑋 ( midG ‘ 𝐺 ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∈ ( 𝐷 𝐿 𝐸 ) ∧ ( ( 𝐷 𝐿 𝐸 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ∨ 𝑋 = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) ) ) ) )
136 83 134 135 mpbir2and ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑋 ) )
137 136 eqcomd ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑋 ) = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) ‘ 𝑌 ) )
138 1 2 3 6 23 24 4 26 17 18 137 lmieq ⊢ ( 𝜑 → 𝑋 = 𝑌 )