Metamath Proof Explorer


Theorem midcom

Description: Commutativity rule for the midpoint. (Contributed by Thierry Arnoux, 2-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 ( 𝜑𝐵𝑃 )
Assertion midcom ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( 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 eqid ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
9 eqid ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
10 1 2 3 4 5 7 6 midcl ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ∈ 𝑃 )
11 eqid ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) )
12 eqidd ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) )
13 1 2 3 4 5 7 6 12 midcgr ( 𝜑 → ( ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) 𝐵 ) = ( ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) 𝐴 ) )
14 1 2 3 4 5 7 6 midbtwn ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ∈ ( 𝐵 𝐼 𝐴 ) )
15 1 2 3 8 9 4 10 11 6 7 13 14 ismir ( 𝜑𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ) ‘ 𝐴 ) )
16 1 2 3 4 5 6 7 9 10 ismidb ( 𝜑 → ( 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ) )
17 15 16 mpbid ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) )