Metamath Proof Explorer


Theorem ragcom

Description: Commutative rule for right angles. Theorem 8.2 of Schwabhauser p. 57. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses israg.p 𝑃 = ( Base ‘ 𝐺 )
israg.d = ( dist ‘ 𝐺 )
israg.i 𝐼 = ( Itv ‘ 𝐺 )
israg.l 𝐿 = ( LineG ‘ 𝐺 )
israg.s 𝑆 = ( pInvG ‘ 𝐺 )
israg.g ( 𝜑𝐺 ∈ TarskiG )
israg.a ( 𝜑𝐴𝑃 )
israg.b ( 𝜑𝐵𝑃 )
israg.c ( 𝜑𝐶𝑃 )
ragcom.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
Assertion ragcom ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 israg.p 𝑃 = ( Base ‘ 𝐺 )
2 israg.d = ( dist ‘ 𝐺 )
3 israg.i 𝐼 = ( Itv ‘ 𝐺 )
4 israg.l 𝐿 = ( LineG ‘ 𝐺 )
5 israg.s 𝑆 = ( pInvG ‘ 𝐺 )
6 israg.g ( 𝜑𝐺 ∈ TarskiG )
7 israg.a ( 𝜑𝐴𝑃 )
8 israg.b ( 𝜑𝐵𝑃 )
9 israg.c ( 𝜑𝐶𝑃 )
10 ragcom.1 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11 eqid ( 𝑆𝐵 ) = ( 𝑆𝐵 )
12 1 2 3 4 5 6 8 11 9 mircl ( 𝜑 → ( ( 𝑆𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
13 1 2 3 4 5 6 7 8 9 israg ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 𝐶 ) = ( 𝐴 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) ) )
14 10 13 mpbid ( 𝜑 → ( 𝐴 𝐶 ) = ( 𝐴 ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) )
15 1 2 3 6 7 9 7 12 14 tgcgrcomlr ( 𝜑 → ( 𝐶 𝐴 ) = ( ( ( 𝑆𝐵 ) ‘ 𝐶 ) 𝐴 ) )
16 1 2 3 4 5 6 8 11 12 7 miriso ( 𝜑 → ( ( ( 𝑆𝐵 ) ‘ ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) ( ( 𝑆𝐵 ) ‘ 𝐴 ) ) = ( ( ( 𝑆𝐵 ) ‘ 𝐶 ) 𝐴 ) )
17 1 2 3 4 5 6 8 11 9 mirmir ( 𝜑 → ( ( 𝑆𝐵 ) ‘ ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) = 𝐶 )
18 17 oveq1d ( 𝜑 → ( ( ( 𝑆𝐵 ) ‘ ( ( 𝑆𝐵 ) ‘ 𝐶 ) ) ( ( 𝑆𝐵 ) ‘ 𝐴 ) ) = ( 𝐶 ( ( 𝑆𝐵 ) ‘ 𝐴 ) ) )
19 15 16 18 3eqtr2d ( 𝜑 → ( 𝐶 𝐴 ) = ( 𝐶 ( ( 𝑆𝐵 ) ‘ 𝐴 ) ) )
20 1 2 3 4 5 6 9 8 7 israg ( 𝜑 → ( ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐶 𝐴 ) = ( 𝐶 ( ( 𝑆𝐵 ) ‘ 𝐴 ) ) ) )
21 19 20 mpbird ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )