Metamath Proof Explorer

Theorem mirval

Description: Value of the point inversion function S . Definition 7.5 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
Assertion mirval ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d ⊢ − = ( dist ‘ 𝐺 )
3 mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 df-mir ⊢ pInvG = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑧 ∈ ( Base ‘ 𝑔 ) ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ) ) ) ) )
9 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
10 9 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
12 11 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = − )
13 12 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 − 𝑧 ) )
14 12 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) = ( 𝑥 − 𝑦 ) )
15 13 14 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ↔ ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ) )
16 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
17 16 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
18 17 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) = ( 𝑧 𝐼 𝑦 ) )
19 18 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ↔ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) )
20 15 19 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ) ↔ ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) )
21 10 20 riotaeqbidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑧 ∈ ( Base ‘ 𝑔 ) ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ) ) = ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) )
22 10 21 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑧 ∈ ( Base ‘ 𝑔 ) ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) )
23 10 22 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑧 ∈ ( Base ‘ 𝑔 ) ( ( 𝑥 ( dist ‘ 𝑔 ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑔 ) 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 ( Itv ‘ 𝑔 ) 𝑦 ) ) ) ) ) = ( 𝑥 ∈ 𝑃 ↦ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ) )
24 6 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
25 1 fvexi ⊢ 𝑃 ∈ V
26 25 mptex ⊢ ( 𝑥 ∈ 𝑃 ↦ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ) ∈ V
27 26 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑃 ↦ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ) ∈ V )
28 8 23 24 27 fvmptd3 ⊢ ( 𝜑 → ( pInvG ‘ 𝐺 ) = ( 𝑥 ∈ 𝑃 ↦ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ) )
29 5 28 syl5eq ⊢ ( 𝜑 → 𝑆 = ( 𝑥 ∈ 𝑃 ↦ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ) )
30 simpll ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑥 = 𝐴 )
31 30 oveq1d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑥 − 𝑧 ) = ( 𝐴 − 𝑧 ) )
32 30 oveq1d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) = ( 𝐴 − 𝑦 ) )
33 31 32 eqeq12d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ↔ ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ) )
34 30 eleq1d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ↔ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) )
35 33 34 anbi12d ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ↔ ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) )
36 35 riotabidva ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 ∈ 𝑃 ) → ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) = ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) )
37 36 mpteq2dva ⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑦 ) ∧ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) )
39 25 mptex ⊢ ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ∈ V
40 39 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) ∈ V )
41 29 38 7 40 fvmptd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑃 ↦ ( ℩ 𝑧 ∈ 𝑃 ( ( 𝐴 − 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ 𝐴 ∈ ( 𝑧 𝐼 𝑦 ) ) ) ) )