Theorem mirrag

Description: Right angle is conserved by point inversion. (Contributed by Thierry Arnoux, 3-Nov-2019)

	Ref	Expression
Hypotheses	israg.p	$$⊢P={\mathrm{Base}}_G$$
	israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	israg.a	$$⊢\phi \to A\in P$$
	israg.b	$$⊢\phi \to B\in P$$
	israg.c	$$⊢\phi \to C\in P$$
	ragmir.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
	mirrag.m	$$⊢M=S\left(D\right)$$
	mirrag.d	$$⊢\phi \to D\in P$$
Assertion	mirrag	$$⊢\phi \to ⟨“M\left(A\right)M\left(B\right)M\left(C\right)”⟩\in {∟}_{𝒢}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$$⊢P={\mathrm{Base}}_G$$
2		israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		israg.a	$$⊢\phi \to A\in P$$
8		israg.b	$$⊢\phi \to B\in P$$
9		israg.c	$$⊢\phi \to C\in P$$
10		ragmir.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
11		mirrag.m	$$⊢M=S\left(D\right)$$
12		mirrag.d	$$⊢\phi \to D\in P$$
13		eqid	$$⊢S\left(B\right)=S\left(B\right)$$
14	1 2 3 4 5 6 8 13 9	mircl	$$⊢\phi \to S\left(B\right)\left(C\right)\in P$$
15	1 2 3 4 5 6 7 8 9	israg	$$⊢\phi \to \left(⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow A\underset{\dot{}}{-}C=A\underset{\dot{}}{-}S\left(B\right)\left(C\right)\right)$$
16	10 15	mpbid	$$⊢\phi \to A\underset{\dot{}}{-}C=A\underset{\dot{}}{-}S\left(B\right)\left(C\right)$$
17	1 2 3 4 5 6 12 11 7 9 7 14 16	mircgrs	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}M\left(C\right)=M\left(A\right)\underset{\dot{}}{-}M\left(S\left(B\right)\left(C\right)\right)$$
18	1 2 3 4 5 6 12 11 9 8	mirmir2	$$⊢\phi \to M\left(S\left(B\right)\left(C\right)\right)=S\left(M\left(B\right)\right)\left(M\left(C\right)\right)$$
19	18	oveq2d	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}M\left(S\left(B\right)\left(C\right)\right)=M\left(A\right)\underset{\dot{}}{-}S\left(M\left(B\right)\right)\left(M\left(C\right)\right)$$
20	17 19	eqtrd	$$⊢\phi \to M\left(A\right)\underset{\dot{}}{-}M\left(C\right)=M\left(A\right)\underset{\dot{}}{-}S\left(M\left(B\right)\right)\left(M\left(C\right)\right)$$
21	1 2 3 4 5 6 12 11 7	mircl	$$⊢\phi \to M\left(A\right)\in P$$
22	1 2 3 4 5 6 12 11 8	mircl	$$⊢\phi \to M\left(B\right)\in P$$
23	1 2 3 4 5 6 12 11 9	mircl	$$⊢\phi \to M\left(C\right)\in P$$
24	1 2 3 4 5 6 21 22 23	israg	$$⊢\phi \to \left(⟨“M\left(A\right)M\left(B\right)M\left(C\right)”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow M\left(A\right)\underset{\dot{}}{-}M\left(C\right)=M\left(A\right)\underset{\dot{}}{-}S\left(M\left(B\right)\right)\left(M\left(C\right)\right)\right)$$
25	20 24	mpbird	$$⊢\phi \to ⟨“M\left(A\right)M\left(B\right)M\left(C\right)”⟩\in {∟}_{𝒢}\left(G\right)$$