Metamath Proof Explorer

Theorem mireq

Description: Equality deduction for point inversion. Theorem 7.9 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 30-May-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 )
mirval.a 
|- ( ph -> A e. P )
mirfv.m 
|- M = ( S ` A )
mirmir.b 
|- ( ph -> B e. P )
mireq.c 
|- ( ph -> C e. P )
mireq.d 
|- ( ph -> ( M ` B ) = ( M ` C ) )
Assertion mireq 
|- ( ph -> B = C )

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 mirval.a 
 |-  ( ph -> A e. P )
8 mirfv.m 
 |-  M = ( S ` A )
9 mirmir.b 
 |-  ( ph -> B e. P )
10 mireq.c 
 |-  ( ph -> C e. P )
11 mireq.d 
 |-  ( ph -> ( M ` B ) = ( M ` C ) )
12 1 2 3 4 5 6 7 8 10 mircl 
 |-  ( ph -> ( M ` C ) e. P )
13 1 2 3 4 5 6 7 8 9 mirfv 
 |-  ( ph -> ( M ` B ) = ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) )
14 13 11 eqtr3d 
 |-  ( ph -> ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) = ( M ` C ) )
15 1 2 3 6 9 7 mirreu3 
 |-  ( ph -> E! z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) )
16 oveq2 
 |-  ( z = ( M ` C ) -> ( A .- z ) = ( A .- ( M ` C ) ) )
17 16 eqeq1d 
 |-  ( z = ( M ` C ) -> ( ( A .- z ) = ( A .- B ) <-> ( A .- ( M ` C ) ) = ( A .- B ) ) )
18 oveq1 
 |-  ( z = ( M ` C ) -> ( z I B ) = ( ( M ` C ) I B ) )
19 18 eleq2d 
 |-  ( z = ( M ` C ) -> ( A e. ( z I B ) <-> A e. ( ( M ` C ) I B ) ) )
20 17 19 anbi12d 
 |-  ( z = ( M ` C ) -> ( ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) <-> ( ( A .- ( M ` C ) ) = ( A .- B ) /\ A e. ( ( M ` C ) I B ) ) ) )
21 20 riota2 
 |-  ( ( ( M ` C ) e. P /\ E! z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) -> ( ( ( A .- ( M ` C ) ) = ( A .- B ) /\ A e. ( ( M ` C ) I B ) ) <-> ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) = ( M ` C ) ) )
22 12 15 21 syl2anc 
 |-  ( ph -> ( ( ( A .- ( M ` C ) ) = ( A .- B ) /\ A e. ( ( M ` C ) I B ) ) <-> ( iota_ z e. P ( ( A .- z ) = ( A .- B ) /\ A e. ( z I B ) ) ) = ( M ` C ) ) )
23 14 22 mpbird 
 |-  ( ph -> ( ( A .- ( M ` C ) ) = ( A .- B ) /\ A e. ( ( M ` C ) I B ) ) )
24 23 simpld 
 |-  ( ph -> ( A .- ( M ` C ) ) = ( A .- B ) )
25 24 eqcomd 
 |-  ( ph -> ( A .- B ) = ( A .- ( M ` C ) ) )
26 23 simprd 
 |-  ( ph -> A e. ( ( M ` C ) I B ) )
27 1 2 3 6 12 7 9 26 tgbtwncom 
 |-  ( ph -> A e. ( B I ( M ` C ) ) )
28 1 2 3 4 5 6 7 8 12 9 25 27 ismir 
 |-  ( ph -> B = ( M ` ( M ` C ) ) )
29 1 2 3 4 5 6 7 8 10 mirmir 
 |-  ( ph -> ( M ` ( M ` C ) ) = C )
30 28 29 eqtrd 
 |-  ( ph -> B = C )