Metamath Proof Explorer

Theorem midf

Description: Midpoint as a function. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismid.d ⊢ − = ( dist ‘ 𝐺 )
ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion midf ( 𝜑 → ( midG ‘ 𝐺 ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 )

Proof

Step Hyp Ref Expression
1 ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismid.d ⊢ − = ( dist ‘ 𝐺 )
3 ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
7 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐺 ∈ TarskiG )
8 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑎 ∈ 𝑃 )
10 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝑏 ∈ 𝑃 )
11 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → 𝐺 DimTarskiG≥ 2 )
12 1 2 3 6 7 8 9 10 11 mideu ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) → ∃! 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) )
13 12 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃! 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) )
14 riotacl ⊢ ( ∃! 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) → ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ∈ 𝑃 )
15 14 2ralimi ⊢ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ∃! 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ∈ 𝑃 )
16 13 15 syl ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ∈ 𝑃 )
17 eqid ⊢ ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) )
18 17 fmpo ⊢ ( ∀ 𝑎 ∈ 𝑃 ∀ 𝑏 ∈ 𝑃 ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ∈ 𝑃 ↔ ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 )
19 16 18 sylib ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 )
20 df-mid ⊢ midG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
21 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
22 21 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
23 fveq2 ⊢ ( 𝑔 = 𝐺 → ( pInvG ‘ 𝑔 ) = ( pInvG ‘ 𝐺 ) )
24 23 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) )
25 24 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) )
26 25 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ↔ 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) )
27 22 26 riotaeqbidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) = ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) )
28 22 22 27 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
29 4 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
30 1 fvexi ⊢ 𝑃 ∈ V
31 30 30 mpoex ⊢ ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) ∈ V
32 31 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) ∈ V )
33 20 28 29 32 fvmptd3 ⊢ ( 𝜑 → ( midG ‘ 𝐺 ) = ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
34 33 feq1d ⊢ ( 𝜑 → ( ( midG ‘ 𝐺 ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 ↔ ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 ) )
35 19 34 mpbird ⊢ ( 𝜑 → ( midG ‘ 𝐺 ) : ( 𝑃 × 𝑃 ) ⟶ 𝑃 )