Theorem perpin

Description: If two lines A and B are perpendicular, then they intersect. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	perpin.1	|- ( ph -> G e. TarskiG )
	perpin.2	|- ( ph -> A ( perpG ` G ) B )
Assertion	perpin	|- ( ph -> ( A i^i B ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		perpin.1	|- ( ph -> G e. TarskiG )
2		perpin.2	|- ( ph -> A ( perpG ` G ) B )
3		ne0i	|- ( x e. ( A i^i B ) -> ( A i^i B ) =/= (/) )
4	3	ad2antlr	|- ( ( ( ph /\ x e. ( A i^i B ) ) /\ A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) -> ( A i^i B ) =/= (/) )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6		eqid	|- ( dist ` G ) = ( dist ` G )
7		eqid	|- ( Itv ` G ) = ( Itv ` G )
8		eqid	|- ( LineG ` G ) = ( LineG ` G )
9	8 1 2	perpln1	|- ( ph -> A e. ran ( LineG ` G ) )
10	8 1 2	perpln2	|- ( ph -> B e. ran ( LineG ` G ) )
11	5 6 7 8 1 9 10	isperp	|- ( ph -> ( A ( perpG ` G ) B <-> E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) ) )
12	2 11	mpbid	|- ( ph -> E. x e. ( A i^i B ) A. u e. A A. v e. B <" u x v "> e. ( raG ` G ) )
13	4 12	r19.29a	|- ( ph -> ( A i^i B ) =/= (/) )