# Metamath Proof Explorer

## Definition df-lmi

Description: Define the line mirroring function. Definition 10.3 of Schwabhauser p. 89. See islmib . (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Assertion df-lmi ${⊢}{lInv}_{𝒢}=\left({g}\in \mathrm{V}⟼\left({m}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)⟼\left({a}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clmi ${class}{lInv}_{𝒢}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 vm ${setvar}{m}$
4 clng ${class}{Line}_{𝒢}$
5 1 cv ${setvar}{g}$
6 5 4 cfv ${class}{Line}_{𝒢}\left({g}\right)$
7 6 crn ${class}\mathrm{ran}{Line}_{𝒢}\left({g}\right)$
8 va ${setvar}{a}$
9 cbs ${class}\mathrm{Base}$
10 5 9 cfv ${class}{\mathrm{Base}}_{{g}}$
11 vb ${setvar}{b}$
12 8 cv ${setvar}{a}$
13 cmid ${class}{mid}_{𝒢}$
14 5 13 cfv ${class}{mid}_{𝒢}\left({g}\right)$
15 11 cv ${setvar}{b}$
16 12 15 14 co ${class}\left({a}{mid}_{𝒢}\left({g}\right){b}\right)$
17 3 cv ${setvar}{m}$
18 16 17 wcel ${wff}{a}{mid}_{𝒢}\left({g}\right){b}\in {m}$
19 cperpg ${class}{⟂}_{𝒢}$
20 5 19 cfv ${class}{⟂}_{𝒢}\left({g}\right)$
21 12 15 6 co ${class}\left({a}{Line}_{𝒢}\left({g}\right){b}\right)$
22 17 21 20 wbr ${wff}{m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)$
23 12 15 wceq ${wff}{a}={b}$
24 22 23 wo ${wff}\left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)$
25 18 24 wa ${wff}\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)$
26 25 11 10 crio ${class}\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)$
27 8 10 26 cmpt ${class}\left({a}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)\right)$
28 3 7 27 cmpt ${class}\left({m}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)⟼\left({a}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)\right)\right)$
29 1 2 28 cmpt ${class}\left({g}\in \mathrm{V}⟼\left({m}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)⟼\left({a}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)\right)\right)\right)$
30 0 29 wceq ${wff}{lInv}_{𝒢}=\left({g}\in \mathrm{V}⟼\left({m}\in \mathrm{ran}{Line}_{𝒢}\left({g}\right)⟼\left({a}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {b}\in {\mathrm{Base}}_{{g}}|\left({a}{mid}_{𝒢}\left({g}\right){b}\in {m}\wedge \left({m}{⟂}_{𝒢}\left({g}\right)\left({a}{Line}_{𝒢}\left({g}\right){b}\right)\vee {a}={b}\right)\right)\right)\right)\right)\right)$