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 28006
Description: Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 28018. (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 28004 . 2 class lInvG
2 vg . . 3 setvar 𝑔
3 cvv 3475 . . 3 class V
4 vm . . . 4 setvar π‘š
52cv 1541 . . . . . 6 class 𝑔
6 clng 27665 . . . . . 6 class LineG
75, 6cfv 6540 . . . . 5 class (LineGβ€˜π‘”)
87crn 5676 . . . 4 class ran (LineGβ€˜π‘”)
9 va . . . . 5 setvar π‘Ž
10 cbs 17140 . . . . . 6 class Base
115, 10cfv 6540 . . . . 5 class (Baseβ€˜π‘”)
129cv 1541 . . . . . . . . 9 class π‘Ž
13 vb . . . . . . . . . 10 setvar 𝑏
1413cv 1541 . . . . . . . . 9 class 𝑏
15 cmid 28003 . . . . . . . . . 10 class midG
165, 15cfv 6540 . . . . . . . . 9 class (midGβ€˜π‘”)
1712, 14, 16co 7404 . . . . . . . 8 class (π‘Ž(midGβ€˜π‘”)𝑏)
184cv 1541 . . . . . . . 8 class π‘š
1917, 18wcel 2107 . . . . . . 7 wff (π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š
2012, 14, 7co 7404 . . . . . . . . 9 class (π‘Ž(LineGβ€˜π‘”)𝑏)
21 cperpg 27926 . . . . . . . . . 10 class βŸ‚G
225, 21cfv 6540 . . . . . . . . 9 class (βŸ‚Gβ€˜π‘”)
2318, 20, 22wbr 5147 . . . . . . . 8 wff π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏)
249, 13weq 1967 . . . . . . . 8 wff π‘Ž = 𝑏
2523, 24wo 846 . . . . . . 7 wff (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏)
2619, 25wa 397 . . . . . 6 wff ((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏))
2726, 13, 11crio 7359 . . . . 5 class (℩𝑏 ∈ (Baseβ€˜π‘”)((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏)))
289, 11, 27cmpt 5230 . . . 4 class (π‘Ž ∈ (Baseβ€˜π‘”) ↦ (℩𝑏 ∈ (Baseβ€˜π‘”)((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏))))
294, 8, 28cmpt 5230 . . 3 class (π‘š ∈ ran (LineGβ€˜π‘”) ↦ (π‘Ž ∈ (Baseβ€˜π‘”) ↦ (℩𝑏 ∈ (Baseβ€˜π‘”)((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏)))))
302, 3, 29cmpt 5230 . 2 class (𝑔 ∈ V ↦ (π‘š ∈ ran (LineGβ€˜π‘”) ↦ (π‘Ž ∈ (Baseβ€˜π‘”) ↦ (℩𝑏 ∈ (Baseβ€˜π‘”)((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏))))))
311, 30wceq 1542 1 wff lInvG = (𝑔 ∈ V ↦ (π‘š ∈ ran (LineGβ€˜π‘”) ↦ (π‘Ž ∈ (Baseβ€˜π‘”) ↦ (℩𝑏 ∈ (Baseβ€˜π‘”)((π‘Ž(midGβ€˜π‘”)𝑏) ∈ π‘š ∧ (π‘š(βŸ‚Gβ€˜π‘”)(π‘Ž(LineGβ€˜π‘”)𝑏) ∨ π‘Ž = 𝑏))))))
Colors of variables: wff setvar class
This definition is referenced by:  lmif  28016  islmib  28018
  Copyright terms: Public domain W3C validator