mirrag

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

	Ref	Expression
Hypotheses	israg.p	\|- P = ( Base ` G )
	israg.d	\|- .- = ( dist ` G )
	israg.i	\|- I = ( Itv ` G )
	israg.l	\|- L = ( LineG ` G )
	israg.s	\|- S = ( pInvG ` G )
	israg.g	\|- ( ph -> G e. TarskiG )
	israg.a	\|- ( ph -> A e. P )
	israg.b	\|- ( ph -> B e. P )
	israg.c	\|- ( ph -> C e. P )
	ragmir.1	\|- ( ph -> <" A B C "> e. ( raG ` G ) )
	mirrag.m	\|- M = ( S ` D )
	mirrag.d	\|- ( ph -> D e. P )
Assertion	mirrag	\|- ( ph -> <" ( M ` A ) ( M ` B ) ( M ` C ) "> e. ( raG ` G ) )

Proof

Step	Hyp	Ref	Expression
1		israg.p	\|- P = ( Base ` G )
2		israg.d	\|- .- = ( dist ` G )
3		israg.i	\|- I = ( Itv ` G )
4		israg.l	\|- L = ( LineG ` G )
5		israg.s	\|- S = ( pInvG ` G )
6		israg.g	\|- ( ph -> G e. TarskiG )
7		israg.a	\|- ( ph -> A e. P )
8		israg.b	\|- ( ph -> B e. P )
9		israg.c	\|- ( ph -> C e. P )
10		ragmir.1	\|- ( ph -> <" A B C "> e. ( raG ` G ) )
11		mirrag.m	\|- M = ( S ` D )
12		mirrag.d	\|- ( ph -> D e. P )
13		eqid	\|- ( S ` B ) = ( S ` B )
14	1 2 3 4 5 6 8 13 9	mircl	\|- ( ph -> ( ( S ` B ) ` C ) e. P )
15	1 2 3 4 5 6 7 8 9	israg	\|- ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
16	10 15	mpbid	\|- ( ph -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
17	1 2 3 4 5 6 12 11 7 9 7 14 16	mircgrs	\|- ( ph -> ( ( M ` A ) .- ( M ` C ) ) = ( ( M ` A ) .- ( M ` ( ( S ` B ) ` C ) ) ) )
18	1 2 3 4 5 6 12 11 9 8	mirmir2	\|- ( ph -> ( M ` ( ( S ` B ) ` C ) ) = ( ( S ` ( M ` B ) ) ` ( M ` C ) ) )
19	18	oveq2d	\|- ( ph -> ( ( M ` A ) .- ( M ` ( ( S ` B ) ` C ) ) ) = ( ( M ` A ) .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) )
20	17 19	eqtrd	\|- ( ph -> ( ( M ` A ) .- ( M ` C ) ) = ( ( M ` A ) .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) )
21	1 2 3 4 5 6 12 11 7	mircl	\|- ( ph -> ( M ` A ) e. P )
22	1 2 3 4 5 6 12 11 8	mircl	\|- ( ph -> ( M ` B ) e. P )
23	1 2 3 4 5 6 12 11 9	mircl	\|- ( ph -> ( M ` C ) e. P )
24	1 2 3 4 5 6 21 22 23	israg	\|- ( ph -> ( <" ( M ` A ) ( M ` B ) ( M ` C ) "> e. ( raG ` G ) <-> ( ( M ` A ) .- ( M ` C ) ) = ( ( M ` A ) .- ( ( S ` ( M ` B ) ) ` ( M ` C ) ) ) ) )
25	20 24	mpbird	\|- ( ph -> <" ( M ` A ) ( M ` B ) ( M ` C ) "> e. ( raG ` G ) )

Metamath Proof Explorer

Theorem mirrag

Proof