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 𝒢 = g ∈ V ⟼ m ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmi class lInv 𝒢
1 vg setvar g
2 cvv class V
3 vm setvar m
4 clng class Line 𝒢
5 1 cv setvar g
6 5 4 cfv class Line 𝒢 ⁡ g
7 6 crn class ran ⁡ Line 𝒢 ⁡ g
8 va setvar a
9 cbs class Base
10 5 9 cfv class Base g
11 vb setvar b
12 8 cv setvar a
13 cmid class mid 𝒢
14 5 13 cfv class mid 𝒢 ⁡ g
15 11 cv setvar b
16 12 15 14 co class a mid 𝒢 ⁡ g b
17 3 cv setvar m
18 16 17 wcel wff a mid 𝒢 ⁡ g b ∈ m
19 cperpg class ⟂ 𝒢
20 5 19 cfv class ⟂ 𝒢 ⁡ g
21 12 15 6 co class a Line 𝒢 ⁡ g b
22 17 21 20 wbr wff m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b
23 12 15 wceq wff a = b
24 22 23 wo wff m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
25 18 24 wa wff a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
26 25 11 10 crio class ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
27 8 10 26 cmpt class a ∈ Base g ⟼ ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
28 3 7 27 cmpt class m ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
29 1 2 28 cmpt class g ∈ V ⟼ m ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b
30 0 29 wceq wff lInv 𝒢 = g ∈ V ⟼ m ∈ ran ⁡ Line 𝒢 ⁡ g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | a mid 𝒢 ⁡ g b ∈ m ∧ m ⟂ 𝒢 ⁡ g a Line 𝒢 ⁡ g b ∨ a = b