Metamath Proof Explorer

Theorem miduniq

Description: Uniqueness of the middle point, expressed with point inversion. Theorem 7.17 of Schwabhauser p. 51. (Contributed by Thierry Arnoux, 30-Jul-2019)

Ref Expression
Hypotheses mirval.p 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
miduniq.a 
|- ( ph -> A e. P )
miduniq.b 
|- ( ph -> B e. P )
miduniq.x 
|- ( ph -> X e. P )
miduniq.y 
|- ( ph -> Y e. P )
miduniq.e 
|- ( ph -> ( ( S ` A ) ` X ) = Y )
miduniq.f 
|- ( ph -> ( ( S ` B ) ` X ) = Y )
Assertion miduniq 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 miduniq.a 
 |-  ( ph -> A e. P )
8 miduniq.b 
 |-  ( ph -> B e. P )
9 miduniq.x 
 |-  ( ph -> X e. P )
10 miduniq.y 
 |-  ( ph -> Y e. P )
11 miduniq.e 
 |-  ( ph -> ( ( S ` A ) ` X ) = Y )
12 miduniq.f 
 |-  ( ph -> ( ( S ` B ) ` X ) = Y )
13 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
14 eqid 
 |-  ( S ` A ) = ( S ` A )
15 1 2 3 4 5 6 7 14 8 mircl 
 |-  ( ph -> ( ( S ` A ) ` B ) e. P )
16 eqid 
 |-  ( S ` B ) = ( S ` B )
17 1 2 3 4 5 6 8 16 9 mirbtwn 
 |-  ( ph -> B e. ( ( ( S ` B ) ` X ) I X ) )
18 12 oveq1d 
 |-  ( ph -> ( ( ( S ` B ) ` X ) I X ) = ( Y I X ) )
19 17 18 eleqtrd 
 |-  ( ph -> B e. ( Y I X ) )
20 1 2 3 6 10 8 9 19 tgbtwncom 
 |-  ( ph -> B e. ( X I Y ) )
21 1 2 3 4 5 6 7 14 10 8 miriso 
 |-  ( ph -> ( ( ( S ` A ) ` Y ) .- ( ( S ` A ) ` B ) ) = ( Y .- B ) )
22 1 2 3 4 5 6 7 14 9 11 mircom 
 |-  ( ph -> ( ( S ` A ) ` Y ) = X )
23 22 oveq1d 
 |-  ( ph -> ( ( ( S ` A ) ` Y ) .- ( ( S ` A ) ` B ) ) = ( X .- ( ( S ` A ) ` B ) ) )
24 1 2 3 4 5 6 8 16 9 mircgr 
 |-  ( ph -> ( B .- ( ( S ` B ) ` X ) ) = ( B .- X ) )
25 12 oveq2d 
 |-  ( ph -> ( B .- ( ( S ` B ) ` X ) ) = ( B .- Y ) )
26 24 25 eqtr3d 
 |-  ( ph -> ( B .- X ) = ( B .- Y ) )
27 26 eqcomd 
 |-  ( ph -> ( B .- Y ) = ( B .- X ) )
28 1 2 3 6 8 10 8 9 27 tgcgrcomlr 
 |-  ( ph -> ( Y .- B ) = ( X .- B ) )
29 21 23 28 3eqtr3rd 
 |-  ( ph -> ( X .- B ) = ( X .- ( ( S ` A ) ` B ) ) )
30 1 2 3 4 5 6 7 14 9 8 miriso 
 |-  ( ph -> ( ( ( S ` A ) ` X ) .- ( ( S ` A ) ` B ) ) = ( X .- B ) )
31 11 oveq1d 
 |-  ( ph -> ( ( ( S ` A ) ` X ) .- ( ( S ` A ) ` B ) ) = ( Y .- ( ( S ` A ) ` B ) ) )
32 1 2 3 6 8 9 8 10 26 tgcgrcomlr 
 |-  ( ph -> ( X .- B ) = ( Y .- B ) )
33 30 31 32 3eqtr3rd 
 |-  ( ph -> ( Y .- B ) = ( Y .- ( ( S ` A ) ` B ) ) )
34 1 4 3 6 9 10 8 13 15 7 2 20 29 33 tgidinside 
 |-  ( ph -> B = ( ( S ` A ) ` B ) )
35 34 eqcomd 
 |-  ( ph -> ( ( S ` A ) ` B ) = B )
36 1 2 3 4 5 6 7 14 8 mirinv 
 |-  ( ph -> ( ( ( S ` A ) ` B ) = B <-> A = B ) )
37 35 36 mpbid 
 |-  ( ph -> A = B )