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

Definition df-lmi 25562
Description: Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 25574. (Contributed by Thierry Arnoux, 1-Dec-2019.)
Assertion
Ref Expression
df-lmi lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))
Distinct variable group:   𝑎,𝑏,𝑔,𝑚

Detailed syntax breakdown of Definition df-lmi
StepHypRef Expression
1 clmi 25560 . 2 class lInvG
2 vg . . 3 setvar 𝑔
3 cvv 3191 . . 3 class V
4 vm . . . 4 setvar 𝑚
52cv 1479 . . . . . 6 class 𝑔
6 clng 25231 . . . . . 6 class LineG
75, 6cfv 5850 . . . . 5 class (LineG‘𝑔)
87crn 5080 . . . 4 class ran (LineG‘𝑔)
9 va . . . . 5 setvar 𝑎
10 cbs 15776 . . . . . 6 class Base
115, 10cfv 5850 . . . . 5 class (Base‘𝑔)
129cv 1479 . . . . . . . . 9 class 𝑎
13 vb . . . . . . . . . 10 setvar 𝑏
1413cv 1479 . . . . . . . . 9 class 𝑏
15 cmid 25559 . . . . . . . . . 10 class midG
165, 15cfv 5850 . . . . . . . . 9 class (midG‘𝑔)
1712, 14, 16co 6605 . . . . . . . 8 class (𝑎(midG‘𝑔)𝑏)
184cv 1479 . . . . . . . 8 class 𝑚
1917, 18wcel 1992 . . . . . . 7 wff (𝑎(midG‘𝑔)𝑏) ∈ 𝑚
2012, 14, 7co 6605 . . . . . . . . 9 class (𝑎(LineG‘𝑔)𝑏)
21 cperpg 25485 . . . . . . . . . 10 class ⟂G
225, 21cfv 5850 . . . . . . . . 9 class (⟂G‘𝑔)
2318, 20, 22wbr 4618 . . . . . . . 8 wff 𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏)
249, 13weq 1876 . . . . . . . 8 wff 𝑎 = 𝑏
2523, 24wo 383 . . . . . . 7 wff (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)
2619, 25wa 384 . . . . . 6 wff ((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))
2726, 13, 11crio 6565 . . . . 5 class (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))
289, 11, 27cmpt 4678 . . . 4 class (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))
294, 8, 28cmpt 4678 . . 3 class (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))
302, 3, 29cmpt 4678 . 2 class (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))
311, 30wceq 1480 1 wff lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))
Colors of variables: wff setvar class
This definition is referenced by:  lmif  25572  islmib  25574
  Copyright terms: Public domain W3C validator