Theorem lmiinv

Description: The invariants of the line mirroring lie on the mirror line. Theorem 10.8 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019)

	Ref	Expression
Hypotheses	ismid.p	|- P = ( Base ` G )
	ismid.d	|- .- = ( dist ` G )
	ismid.i	|- I = ( Itv ` G )
	ismid.g	|- ( ph -> G e. TarskiG )
	ismid.1	|- ( ph -> G TarskiGDim>= 2 )
	lmif.m	|- M = ( ( lInvG ` G ) ` D )
	lmif.l	|- L = ( LineG ` G )
	lmif.d	|- ( ph -> D e. ran L )
	lmicl.1	|- ( ph -> A e. P )
Assertion	lmiinv	|- ( ph -> ( ( M ` A ) = A <-> A e. D ) )

Proof

Step	Hyp	Ref	Expression
1		ismid.p	|- P = ( Base ` G )
2		ismid.d	|- .- = ( dist ` G )
3		ismid.i	|- I = ( Itv ` G )
4		ismid.g	|- ( ph -> G e. TarskiG )
5		ismid.1	|- ( ph -> G TarskiGDim>= 2 )
6		lmif.m	|- M = ( ( lInvG ` G ) ` D )
7		lmif.l	|- L = ( LineG ` G )
8		lmif.d	|- ( ph -> D e. ran L )
9		lmicl.1	|- ( ph -> A e. P )
10	1 2 3 4 5 6 7 8 9 9	islmib	|- ( ph -> ( A = ( M ` A ) <-> ( ( A ( midG ` G ) A ) e. D /\ ( D ( perpG ` G ) ( A L A ) \/ A = A ) ) ) )
11		eqcom	|- ( A = ( M ` A ) <-> ( M ` A ) = A )
12	11	a1i	|- ( ph -> ( A = ( M ` A ) <-> ( M ` A ) = A ) )
13		eqidd	|- ( ph -> A = A )
14	13	olcd	|- ( ph -> ( D ( perpG ` G ) ( A L A ) \/ A = A ) )
15	14	biantrud	|- ( ph -> ( ( A ( midG ` G ) A ) e. D <-> ( ( A ( midG ` G ) A ) e. D /\ ( D ( perpG ` G ) ( A L A ) \/ A = A ) ) ) )
16	1 2 3 4 5 9 9	midid	|- ( ph -> ( A ( midG ` G ) A ) = A )
17	16	eleq1d	|- ( ph -> ( ( A ( midG ` G ) A ) e. D <-> A e. D ) )
18	15 17	bitr3d	|- ( ph -> ( ( ( A ( midG ` G ) A ) e. D /\ ( D ( perpG ` G ) ( A L A ) \/ A = A ) ) <-> A e. D ) )
19	10 12 18	3bitr3d	|- ( ph -> ( ( M ` A ) = A <-> A e. D ) )