Theorem isperp2d

Description: One direction of isperp2 . (Contributed by Thierry Arnoux, 10-Nov-2019)

	Ref	Expression
Hypotheses	isperp.p	|- P = ( Base ` G )
	isperp.d	|- .- = ( dist ` G )
	isperp.i	|- I = ( Itv ` G )
	isperp.l	|- L = ( LineG ` G )
	isperp.g	|- ( ph -> G e. TarskiG )
	isperp.a	|- ( ph -> A e. ran L )
	isperp2.b	|- ( ph -> B e. ran L )
	isperp2.x	|- ( ph -> X e. ( A i^i B ) )
	isperp2d.u	|- ( ph -> U e. A )
	isperp2d.v	|- ( ph -> V e. B )
	isperp2d.p	|- ( ph -> A ( perpG ` G ) B )
Assertion	isperp2d	|- ( ph -> <" U X V "> e. ( raG ` G ) )

Proof

Step	Hyp	Ref	Expression
1		isperp.p	|- P = ( Base ` G )
2		isperp.d	|- .- = ( dist ` G )
3		isperp.i	|- I = ( Itv ` G )
4		isperp.l	|- L = ( LineG ` G )
5		isperp.g	|- ( ph -> G e. TarskiG )
6		isperp.a	|- ( ph -> A e. ran L )
7		isperp2.b	|- ( ph -> B e. ran L )
8		isperp2.x	|- ( ph -> X e. ( A i^i B ) )
9		isperp2d.u	|- ( ph -> U e. A )
10		isperp2d.v	|- ( ph -> V e. B )
11		isperp2d.p	|- ( ph -> A ( perpG ` G ) B )
12	1 2 3 4 5 6 7 8	isperp2	|- ( ph -> ( A ( perpG ` G ) B <-> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) ) )
13	11 12	mpbid	|- ( ph -> A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) )
14		id	|- ( u = U -> u = U )
15		eqidd	|- ( u = U -> X = X )
16		eqidd	|- ( u = U -> v = v )
17	14 15 16	s3eqd	|- ( u = U -> <" u X v "> = <" U X v "> )
18	17	eleq1d	|- ( u = U -> ( <" u X v "> e. ( raG ` G ) <-> <" U X v "> e. ( raG ` G ) ) )
19		eqidd	|- ( v = V -> U = U )
20		eqidd	|- ( v = V -> X = X )
21		id	|- ( v = V -> v = V )
22	19 20 21	s3eqd	|- ( v = V -> <" U X v "> = <" U X V "> )
23	22	eleq1d	|- ( v = V -> ( <" U X v "> e. ( raG ` G ) <-> <" U X V "> e. ( raG ` G ) ) )
24	18 23	rspc2v	|- ( ( U e. A /\ V e. B ) -> ( A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) -> <" U X V "> e. ( raG ` G ) ) )
25	9 10 24	syl2anc	|- ( ph -> ( A. u e. A A. v e. B <" u X v "> e. ( raG ` G ) -> <" U X V "> e. ( raG ` G ) ) )
26	13 25	mpd	|- ( ph -> <" U X V "> e. ( raG ` G ) )