Theorem ismidb

Description: Property of the midpoint. (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 )
	midcl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	midcl.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	ismidb.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	ismidb.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
Assertion	ismidb	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) ↔ ( 𝐴 ( 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		midcl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		midcl.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		ismidb.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
9		ismidb.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
10		eqid	⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
11	1 2 3 10 4 8 6 7 5	mideu	⊢ ( 𝜑 → ∃! 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) )
12		fveq2	⊢ ( 𝑚 = 𝑀 → ( 𝑆 ‘ 𝑚 ) = ( 𝑆 ‘ 𝑀 ) )
13	12	fveq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) )
14	13	eqeq2d	⊢ ( 𝑚 = 𝑀 → ( 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ↔ 𝐵 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) ) )
15	14	riota2	⊢ ( ( 𝑀 ∈ 𝑃 ∧ ∃! 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) → ( 𝐵 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) ↔ ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) = 𝑀 ) )
16	9 11 15	syl2anc	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) ↔ ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) = 𝑀 ) )
17		df-mid	⊢ midG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
18		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
19	18 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
20		fveq2	⊢ ( 𝑔 = 𝐺 → ( pInvG ‘ 𝑔 ) = ( pInvG ‘ 𝐺 ) )
21	20 8	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( pInvG ‘ 𝑔 ) = 𝑆 )
22	21	fveq1d	⊢ ( 𝑔 = 𝐺 → ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) = ( 𝑆 ‘ 𝑚 ) )
23	22	fveq1d	⊢ ( 𝑔 = 𝐺 → ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) )
24	23	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ↔ 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) )
25	19 24	riotaeqbidv	⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) = ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) )
26	19 19 25	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
27	4	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
28	1	fvexi	⊢ 𝑃 ∈ V
29	28 28	mpoex	⊢ ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) ) ∈ V
30	29	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) ) ∈ V )
31	17 26 27 30	fvmptd3	⊢ ( 𝜑 → ( midG ‘ 𝐺 ) = ( 𝑎 ∈ 𝑃 , 𝑏 ∈ 𝑃 ↦ ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
32		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → 𝑏 = 𝐵 )
33		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → 𝑎 = 𝐴 )
34	33	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) )
35	32 34	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ↔ 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) )
36	35	riotabidv	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( ℩ 𝑚 ∈ 𝑃 𝑏 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝑎 ) ) = ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) )
37		riotacl	⊢ ( ∃! 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) → ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) ∈ 𝑃 )
38	11 37	syl	⊢ ( 𝜑 → ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) ∈ 𝑃 )
39	31 36 6 7 38	ovmpod	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) )
40	39	eqeq1d	⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = 𝑀 ↔ ( ℩ 𝑚 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑚 ) ‘ 𝐴 ) ) = 𝑀 ) )
41	16 40	bitr4d	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝑆 ‘ 𝑀 ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = 𝑀 ) )