Metamath Proof Explorer

Theorem plngrot

Description: The plane defined by a line ( X L Y ) and a point Z is also defined by the line ( Z L Y ) and the point X . See first part of Theorem 9.24 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 )
plngrot.x 
|- ( ph -> X e. ( P \ ( Z L Y ) ) )
plngrot.y 
|- ( ph -> Y e. P )
plngrot.z 
|- ( ph -> Z e. ( P \ ( X L Y ) ) )
plngrot.1 
|- ( ph -> X =/= Y )
Assertion plngrot 
|- ( ph -> ( ( X L Y ) E Z ) = ( ( Z L Y ) E X ) )

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 plngrot.x 
 |-  ( ph -> X e. ( P \ ( Z L Y ) ) )
7 plngrot.y 
 |-  ( ph -> Y e. P )
8 plngrot.z 
 |-  ( ph -> Z e. ( P \ ( X L Y ) ) )
9 plngrot.1 
 |-  ( ph -> X =/= Y )
10 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
11 eleq1w 
 |-  ( a = c -> ( a e. ( P \ ( X L Y ) ) <-> c e. ( P \ ( X L Y ) ) ) )
12 eleq1w 
 |-  ( b = d -> ( b e. ( P \ ( X L Y ) ) <-> d e. ( P \ ( X L Y ) ) ) )
13 11 12 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( X L Y ) ) /\ b e. ( P \ ( X L Y ) ) ) <-> ( c e. ( P \ ( X L Y ) ) /\ d e. ( P \ ( X L Y ) ) ) ) )
14 eleq1w 
 |-  ( t = u -> ( t e. ( a ( Itv ` G ) b ) <-> u e. ( a ( Itv ` G ) b ) ) )
15 14 cbvrexvw 
 |-  ( E. t e. ( X L Y ) t e. ( a ( Itv ` G ) b ) <-> E. u e. ( X L Y ) u e. ( a ( Itv ` G ) b ) )
16 oveq12 
 |-  ( ( a = c /\ b = d ) -> ( a ( Itv ` G ) b ) = ( c ( Itv ` G ) d ) )
17 16 eleq2d 
 |-  ( ( a = c /\ b = d ) -> ( u e. ( a ( Itv ` G ) b ) <-> u e. ( c ( Itv ` G ) d ) ) )
18 17 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. u e. ( X L Y ) u e. ( a ( Itv ` G ) b ) <-> E. u e. ( X L Y ) u e. ( c ( Itv ` G ) d ) ) )
19 15 18 bitrid 
 |-  ( ( a = c /\ b = d ) -> ( E. t e. ( X L Y ) t e. ( a ( Itv ` G ) b ) <-> E. u e. ( X L Y ) u e. ( c ( Itv ` G ) d ) ) )
20 13 19 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( X L Y ) ) /\ b e. ( P \ ( X L Y ) ) ) /\ E. t e. ( X L Y ) t e. ( a ( Itv ` G ) b ) ) <-> ( ( c e. ( P \ ( X L Y ) ) /\ d e. ( P \ ( X L Y ) ) ) /\ E. u e. ( X L Y ) u e. ( c ( Itv ` G ) d ) ) ) )
21 20 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( X L Y ) ) /\ b e. ( P \ ( X L Y ) ) ) /\ E. t e. ( X L Y ) t e. ( a ( Itv ` G ) b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( X L Y ) ) /\ d e. ( P \ ( X L Y ) ) ) /\ E. u e. ( X L Y ) u e. ( c ( Itv ` G ) d ) ) }
22 1 10 3 4 5 6 7 8 9 21 plngrotlem3 
 |-  ( ph -> ( ( X L Y ) E Z ) C_ ( ( Z L Y ) E X ) )
23 6 eldifad 
 |-  ( ph -> X e. P )
24 1 2 3 5 23 7 9 tglinerflx2 
 |-  ( ph -> Y e. ( X L Y ) )
25 8 eldifbd 
 |-  ( ph -> -. Z e. ( X L Y ) )
26 nelne2 
 |-  ( ( Y e. ( X L Y ) /\ -. Z e. ( X L Y ) ) -> Y =/= Z )
27 24 25 26 syl2anc 
 |-  ( ph -> Y =/= Z )
28 27 necomd 
 |-  ( ph -> Z =/= Y )
29 eleq1w 
 |-  ( a = c -> ( a e. ( P \ ( Z L Y ) ) <-> c e. ( P \ ( Z L Y ) ) ) )
30 eleq1w 
 |-  ( b = d -> ( b e. ( P \ ( Z L Y ) ) <-> d e. ( P \ ( Z L Y ) ) ) )
31 29 30 bi2anan9 
 |-  ( ( a = c /\ b = d ) -> ( ( a e. ( P \ ( Z L Y ) ) /\ b e. ( P \ ( Z L Y ) ) ) <-> ( c e. ( P \ ( Z L Y ) ) /\ d e. ( P \ ( Z L Y ) ) ) ) )
32 14 cbvrexvw 
 |-  ( E. t e. ( Z L Y ) t e. ( a ( Itv ` G ) b ) <-> E. u e. ( Z L Y ) u e. ( a ( Itv ` G ) b ) )
33 17 rexbidv 
 |-  ( ( a = c /\ b = d ) -> ( E. u e. ( Z L Y ) u e. ( a ( Itv ` G ) b ) <-> E. u e. ( Z L Y ) u e. ( c ( Itv ` G ) d ) ) )
34 32 33 bitrid 
 |-  ( ( a = c /\ b = d ) -> ( E. t e. ( Z L Y ) t e. ( a ( Itv ` G ) b ) <-> E. u e. ( Z L Y ) u e. ( c ( Itv ` G ) d ) ) )
35 31 34 anbi12d 
 |-  ( ( a = c /\ b = d ) -> ( ( ( a e. ( P \ ( Z L Y ) ) /\ b e. ( P \ ( Z L Y ) ) ) /\ E. t e. ( Z L Y ) t e. ( a ( Itv ` G ) b ) ) <-> ( ( c e. ( P \ ( Z L Y ) ) /\ d e. ( P \ ( Z L Y ) ) ) /\ E. u e. ( Z L Y ) u e. ( c ( Itv ` G ) d ) ) ) )
36 35 cbvopabv 
 |-  { <. a , b >. | ( ( a e. ( P \ ( Z L Y ) ) /\ b e. ( P \ ( Z L Y ) ) ) /\ E. t e. ( Z L Y ) t e. ( a ( Itv ` G ) b ) ) } = { <. c , d >. | ( ( c e. ( P \ ( Z L Y ) ) /\ d e. ( P \ ( Z L Y ) ) ) /\ E. u e. ( Z L Y ) u e. ( c ( Itv ` G ) d ) ) }
37 1 10 3 4 5 8 7 6 28 36 plngrotlem3 
 |-  ( ph -> ( ( Z L Y ) E X ) C_ ( ( X L Y ) E Z ) )
38 22 37 eqssd 
 |-  ( ph -> ( ( X L Y ) E Z ) = ( ( Z L Y ) E X ) )