Theorem plngcp

Description: The plane defined by a line A and a point R can also be defined using a different point R on the same plane: changes the point used to define the plane. Theorem 9.21 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 )
	plngcp.a	|- ( ph -> A e. ran L )
	plngcp.r	|- ( ph -> R e. ( P \ A ) )
	plngcp.s	|- ( ph -> S e. ( ( A E R ) \ A ) )
Assertion	plngcp	|- ( ph -> ( A E R ) = ( A E S ) )

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		plngcp.a	|- ( ph -> A e. ran L )
7		plngcp.r	|- ( ph -> R e. ( P \ A ) )
8		plngcp.s	|- ( ph -> S e. ( ( A E R ) \ A ) )
9		eleq1w	|- ( a = c -> ( a e. ( P \ A ) <-> c e. ( P \ A ) ) )
10		eleq1w	|- ( b = d -> ( b e. ( P \ A ) <-> d e. ( P \ A ) ) )
11	9 10	bi2anan9	|- ( ( a = c /\ b = d ) -> ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) <-> ( c e. ( P \ A ) /\ d e. ( P \ A ) ) ) )
12		eleq1w	|- ( t = s -> ( t e. ( a I b ) <-> s e. ( a I b ) ) )
13	12	cbvrexvw	|- ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( a I b ) )
14		oveq12	|- ( ( a = c /\ b = d ) -> ( a I b ) = ( c I d ) )
15	14	eleq2d	|- ( ( a = c /\ b = d ) -> ( s e. ( a I b ) <-> s e. ( c I d ) ) )
16	15	rexbidv	|- ( ( a = c /\ b = d ) -> ( E. s e. A s e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
17	13 16	bitrid	|- ( ( a = c /\ b = d ) -> ( E. t e. A t e. ( a I b ) <-> E. s e. A s e. ( c I d ) ) )
18	11 17	anbi12d	|- ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) <-> ( ( c e. ( P \ A ) /\ d e. ( P \ A ) ) /\ E. s e. A s e. ( c I d ) ) ) )
19	18	cbvopabv	|- { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) } = { <. c , d >. | ( ( c e. ( P \ A ) /\ d e. ( P \ A ) ) /\ E. s e. A s e. ( c I d ) ) }
20	1 2 3 4 5 6 7 8 19	plngcplem	|- ( ph -> ( A E R ) = ( A E S ) )