elplng

Description: Elementhood in the plane defined by a line A and a point R . Definition 9.20 of Schwabhauser p. 74. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	\|- P = ( Base ` G )
	plngval.i	\|- I = ( Itv ` G )
	plngval.1	\|- L = ( LineG ` G )
	plngval.e	\|- E = ( PlnG ` G )
	plngval.g	\|- ( ph -> G e. TarskiG )
	elplng.a	\|- ( ph -> A e. ran L )
	elplng.r	\|- ( ph -> R e. ( P \ A ) )
	elplng.o	\|- O = { <. a , b >. \| ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
	elplng.x	\|- ( ph -> X e. P )
Assertion	elplng	\|- ( ph -> ( X e. ( A E R ) <-> ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )

Proof

Step	Hyp	Ref	Expression
1		plngval.p	\|- P = ( Base ` G )
2		plngval.i	\|- I = ( Itv ` G )
3		plngval.1	\|- L = ( LineG ` G )
4		plngval.e	\|- E = ( PlnG ` G )
5		plngval.g	\|- ( ph -> G e. TarskiG )
6		elplng.a	\|- ( ph -> A e. ran L )
7		elplng.r	\|- ( ph -> R e. ( P \ A ) )
8		elplng.o	\|- O = { <. a , b >. \| ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
9		elplng.x	\|- ( ph -> X e. P )
10	1 2 3 4 5 6 7	plngval	\|- ( ph -> ( A E R ) = { x e. P \| ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } )
11	10	eleq2d	\|- ( ph -> ( X e. ( A E R ) <-> X e. { x e. P \| ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } ) )
12		eleq1	\|- ( x = X -> ( x e. A <-> X e. A ) )
13		breq1	\|- ( x = X -> ( x ( ( hpG ` G ) ` A ) R <-> X ( ( hpG ` G ) ` A ) R ) )
14		oveq1	\|- ( x = X -> ( x I R ) = ( X I R ) )
15	14	eleq2d	\|- ( x = X -> ( t e. ( x I R ) <-> t e. ( X I R ) ) )
16	15	rexbidv	\|- ( x = X -> ( E. t e. A t e. ( x I R ) <-> E. t e. A t e. ( X I R ) ) )
17	12 13 16	3orbi123d	\|- ( x = X -> ( ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) <-> ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) )
18	17	elrab	\|- ( X e. { x e. P \| ( x e. A \/ x ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( x I R ) ) } <-> ( X e. P /\ ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) )
19	11 18	bitrdi	\|- ( ph -> ( X e. ( A E R ) <-> ( X e. P /\ ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) ) )
20	9	biantrurd	\|- ( ph -> ( ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) <-> ( X e. P /\ ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) ) )
21	7	eldifbd	\|- ( ph -> -. R e. A )
22	21	anim1ci	\|- ( ( ph /\ -. X e. A ) -> ( -. X e. A /\ -. R e. A ) )
23	22	biantrurd	\|- ( ( ph /\ -. X e. A ) -> ( E. t e. A t e. ( X I R ) <-> ( ( -. X e. A /\ -. R e. A ) /\ E. t e. A t e. ( X I R ) ) ) )
24		eqid	\|- ( dist ` G ) = ( dist ` G )
25	9	adantr	\|- ( ( ph /\ -. X e. A ) -> X e. P )
26	7	eldifad	\|- ( ph -> R e. P )
27	26	adantr	\|- ( ( ph /\ -. X e. A ) -> R e. P )
28	1 24 2 8 25 27	islnopp	\|- ( ( ph /\ -. X e. A ) -> ( X O R <-> ( ( -. X e. A /\ -. R e. A ) /\ E. t e. A t e. ( X I R ) ) ) )
29	23 28	bitr4d	\|- ( ( ph /\ -. X e. A ) -> ( E. t e. A t e. ( X I R ) <-> X O R ) )
30	29	orbi2d	\|- ( ( ph /\ -. X e. A ) -> ( ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) <-> ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )
31	30	pm5.74da	\|- ( ph -> ( ( -. X e. A -> ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) <-> ( -. X e. A -> ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) ) )
32		df-or	\|- ( ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) <-> ( -. X e. A -> ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) )
33		df-or	\|- ( ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) <-> ( -. X e. A -> ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )
34	31 32 33	3bitr4g	\|- ( ph -> ( ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) <-> ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) ) )
35		3orass	\|- ( ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) <-> ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) ) )
36		3orass	\|- ( ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ X O R ) <-> ( X e. A \/ ( X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )
37	34 35 36	3bitr4g	\|- ( ph -> ( ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ E. t e. A t e. ( X I R ) ) <-> ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )
38	19 20 37	3bitr2d	\|- ( ph -> ( X e. ( A E R ) <-> ( X e. A \/ X ( ( hpG ` G ) ` A ) R \/ X O R ) ) )

Metamath Proof Explorer

Theorem elplng

Proof