Description: Equality deduction for line mirroring. Theorem 10.7 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismid.p | |- P = ( Base ` G ) |
|
ismid.d | |- .- = ( dist ` G ) |
||
ismid.i | |- I = ( Itv ` G ) |
||
ismid.g | |- ( ph -> G e. TarskiG ) |
||
ismid.1 | |- ( ph -> G TarskiGDim>= 2 ) |
||
lmif.m | |- M = ( ( lInvG ` G ) ` D ) |
||
lmif.l | |- L = ( LineG ` G ) |
||
lmif.d | |- ( ph -> D e. ran L ) |
||
lmicl.1 | |- ( ph -> A e. P ) |
||
lmieq.c | |- ( ph -> B e. P ) |
||
lmieq.d | |- ( ph -> ( M ` A ) = ( M ` B ) ) |
||
Assertion | lmieq | |- ( ph -> A = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismid.p | |- P = ( Base ` G ) |
|
2 | ismid.d | |- .- = ( dist ` G ) |
|
3 | ismid.i | |- I = ( Itv ` G ) |
|
4 | ismid.g | |- ( ph -> G e. TarskiG ) |
|
5 | ismid.1 | |- ( ph -> G TarskiGDim>= 2 ) |
|
6 | lmif.m | |- M = ( ( lInvG ` G ) ` D ) |
|
7 | lmif.l | |- L = ( LineG ` G ) |
|
8 | lmif.d | |- ( ph -> D e. ran L ) |
|
9 | lmicl.1 | |- ( ph -> A e. P ) |
|
10 | lmieq.c | |- ( ph -> B e. P ) |
|
11 | lmieq.d | |- ( ph -> ( M ` A ) = ( M ` B ) ) |
|
12 | fveqeq2 | |- ( b = A -> ( ( M ` b ) = ( M ` B ) <-> ( M ` A ) = ( M ` B ) ) ) |
|
13 | fveqeq2 | |- ( b = B -> ( ( M ` b ) = ( M ` B ) <-> ( M ` B ) = ( M ` B ) ) ) |
|
14 | 1 2 3 4 5 6 7 8 10 | lmicl | |- ( ph -> ( M ` B ) e. P ) |
15 | 1 2 3 4 5 6 7 8 14 | lmireu | |- ( ph -> E! b e. P ( M ` b ) = ( M ` B ) ) |
16 | eqidd | |- ( ph -> ( M ` B ) = ( M ` B ) ) |
|
17 | 12 13 15 9 10 11 16 | reu2eqd | |- ( ph -> A = B ) |