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 |
|
midcl.1 |
|- ( ph -> A e. P ) |
7 |
|
midcl.2 |
|- ( ph -> B e. P ) |
8 |
1 2 3 4 5 6 7
|
midcl |
|- ( ph -> ( A ( midG ` G ) B ) e. P ) |
9 |
|
eqid |
|- ( LineG ` G ) = ( LineG ` G ) |
10 |
|
eqid |
|- ( pInvG ` G ) = ( pInvG ` G ) |
11 |
|
eqid |
|- ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) |
12 |
1 2 3 9 10 4 8 11 6
|
mirbtwn |
|- ( ph -> ( A ( midG ` G ) B ) e. ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) I A ) ) |
13 |
|
eqidd |
|- ( ph -> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) ) |
14 |
1 2 3 4 5 6 7 10 8
|
ismidb |
|- ( ph -> ( B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) <-> ( A ( midG ` G ) B ) = ( A ( midG ` G ) B ) ) ) |
15 |
13 14
|
mpbird |
|- ( ph -> B = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) ) |
16 |
15
|
oveq1d |
|- ( ph -> ( B I A ) = ( ( ( ( pInvG ` G ) ` ( A ( midG ` G ) B ) ) ` A ) I A ) ) |
17 |
12 16
|
eleqtrrd |
|- ( ph -> ( A ( midG ` G ) B ) e. ( B I A ) ) |
18 |
1 2 3 4 7 8 6 17
|
tgbtwncom |
|- ( ph -> ( A ( midG ` G ) B ) e. ( A I B ) ) |