Metamath Proof Explorer

Theorem mirrag

Description: Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-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 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
ragmir.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
mirrag.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐷 )
mirrag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
Assertion mirrag ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝐴 ) ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟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 ragmir.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11 mirrag.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐷 )
12 mirrag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
13 eqid ⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
14 1 2 3 4 5 6 8 13 9 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ∈ 𝑃 )
15 1 2 3 4 5 6 7 8 9 israg ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )
16 10 15 mpbid ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) )
17 1 2 3 4 5 6 12 11 7 9 7 14 16 mircgrs ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐶 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) )
18 1 2 3 4 5 6 12 11 9 8 mirmir2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) )
19 18 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐶 ) ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) ) )
20 17 19 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐶 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) ) )
21 1 2 3 4 5 6 12 11 7 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )
22 1 2 3 4 5 6 12 11 8 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ 𝑃 )
23 1 2 3 4 5 6 12 11 9 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐶 ) ∈ 𝑃 )
24 1 2 3 4 5 6 21 22 23 israg ⊢ ( 𝜑 → ( ⟨“ ( 𝑀 ‘ 𝐴 ) ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( ( 𝑀 ‘ 𝐴 ) − ( 𝑀 ‘ 𝐶 ) ) = ( ( 𝑀 ‘ 𝐴 ) − ( ( 𝑆 ‘ ( 𝑀 ‘ 𝐵 ) ) ‘ ( 𝑀 ‘ 𝐶 ) ) ) ) )
25 20 24 mpbird ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝐴 ) ( 𝑀 ‘ 𝐵 ) ( 𝑀 ‘ 𝐶 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )