Theorem plngval

Description: The plane defined by a line A and a point R outside of A . This is defined as the union of 3 parts: the line itself, the open half-plane containing R , and the points opposite to R (see islnopp ). (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	plngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	plngval.1	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	plngval.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	plngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	plngval.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	plngval.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
Assertion	plngval	⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		plngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		plngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		plngval.1	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		plngval.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
5		plngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		plngval.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7		plngval.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
8		df-plng	⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )
9		fveq2	⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
10	9 3	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
11	10	rneqd	⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
12		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
13	12 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
14	13	difeq1d	⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) = ( 𝑃 ∖ 𝑎 ) )
15		biidd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝑎 ) )
16		fveq2	⊢ ( 𝑔 = 𝐺 → ( hpG ‘ 𝑔 ) = ( hpG ‘ 𝐺 ) )
17	16	fveq1d	⊢ ( 𝑔 = 𝐺 → ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) = ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) )
18	17	breqd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ) )
19		fveq2	⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
20	19 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
21	20	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) = ( 𝑥 𝐼 𝑟 ) )
22	21	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) )
23	22	rexbidv	⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) )
24	15 18 23	3orbi123d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) ↔ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) ) )
25	13 24	rabeqbidv	⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
26	11 14 25	mpoeq123dv	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
27	5	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
28	3	fvexi	⊢ 𝐿 ∈ V
29	28	rnex	⊢ ran 𝐿 ∈ V
30	29	a1i	⊢ ( 𝜑 → ran 𝐿 ∈ V )
31	1	fvexi	⊢ 𝑃 ∈ V
32	31	difexi	⊢ ( 𝑃 ∖ 𝑎 ) ∈ V
33	32	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) → ( 𝑃 ∖ 𝑎 ) ∈ V )
34	30 33	mpoexd	⊢ ( 𝜑 → ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) ∈ V )
35	8 26 27 34	fvmptd3	⊢ ( 𝜑 → ( hlG ‘ 𝐺 ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
36	4 35	eqtrid	⊢ ( 𝜑 → 𝐸 = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
37	7	adantr	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
38		difeq2	⊢ ( 𝑎 = 𝐴 → ( 𝑃 ∖ 𝑎 ) = ( 𝑃 ∖ 𝐴 ) )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( 𝑃 ∖ 𝑎 ) = ( 𝑃 ∖ 𝐴 ) )
40	37 39	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → 𝑅 ∈ ( 𝑃 ∖ 𝑎 ) )
41		eqid	⊢ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) }
42	31	a1i	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → 𝑃 ∈ V )
43	41 42	rabexd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ∈ V )
44		eleq2w2	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) )
45	44	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) )
46		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → 𝑥 = 𝑥 )
47		fveq2	⊢ ( 𝑎 = 𝐴 → ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) = ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) )
48	47	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) = ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) )
49		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → 𝑟 = 𝑅 )
50	46 48 49	breq123d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ) )
51		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → 𝑎 = 𝐴 )
52	49	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( 𝑥 𝐼 𝑟 ) = ( 𝑥 𝐼 𝑅 ) )
53	52	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ↔ 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) )
54	51 53	rexeqbidv	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) )
55	45 50 54	3orbi123d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → ( ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) ) )
56	55	rabbidv	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑟 = 𝑅 ) ) → { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )
57	6 40 43 56	ovmpodv2	⊢ ( 𝜑 → ( 𝐸 = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } ) )
58	36 57	mpd	⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑅 ∨ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ) } )