Metamath Proof Explorer

Theorem tgaltai

Description: Parallelism implies alternate angles congruence: if a line ( X L Z ) crosses two parallel lines ( X L Y ) and ( Z L W ) , then the alternate angles are congruent. First direction of Theorem 12.21 of Schwabhauser p. 126. This is also Proposition 1.29 of Euclid's Elements . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses tgaltai.p 
|- P = ( Base ` G )
tgaltai.i 
|- I = ( Itv ` G )
tgaltai.l 
|- L = ( LineG ` G )
tgaltai.r 
|- .|| = ( parlnG ` G )
tgaltai.o 
|- O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
tgaltai.g 
|- ( ph -> G e. TarskiG )
tgaltai.1 
|- ( ph -> G e. TarskiGE )
tgaltai.x 
|- ( ph -> X e. P )
tgaltai.y 
|- ( ph -> Y e. P )
tgaltai.z 
|- ( ph -> Z e. P )
tgaltai.w 
|- ( ph -> W e. P )
tgaltai.2 
|- ( ph -> ( X L Y ) .|| ( Z L W ) )
tgaltai.3 
|- ( ph -> Y O W )
tgaltai.4 
|- ( ph -> X =/= Z )
Assertion tgaltai 
|- ( ph -> <" Y X Z "> ( cgrA ` G ) <" W Z X "> )

Proof

Step Hyp Ref Expression
1 tgaltai.p 
 |-  P = ( Base ` G )
2 tgaltai.i 
 |-  I = ( Itv ` G )
3 tgaltai.l 
 |-  L = ( LineG ` G )
4 tgaltai.r 
 |-  .|| = ( parlnG ` G )
5 tgaltai.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) }
6 tgaltai.g 
 |-  ( ph -> G e. TarskiG )
7 tgaltai.1 
 |-  ( ph -> G e. TarskiGE )
8 tgaltai.x 
 |-  ( ph -> X e. P )
9 tgaltai.y 
 |-  ( ph -> Y e. P )
10 tgaltai.z 
 |-  ( ph -> Z e. P )
11 tgaltai.w 
 |-  ( ph -> W e. P )
12 tgaltai.2 
 |-  ( ph -> ( X L Y ) .|| ( Z L W ) )
13 tgaltai.3 
 |-  ( ph -> Y O W )
14 tgaltai.4 
 |-  ( ph -> X =/= Z )
15 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
16 6 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> G e. TarskiG )
17 9 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Y e. P )
18 8 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> X e. P )
19 10 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Z e. P )
20 11 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> W e. P )
21 simplr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t e. P )
22 eqid 
 |-  ( dist ` G ) = ( dist ` G )
23 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
24 simprr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) )
25 24 eqcomd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( X ( dist ` G ) Y ) = ( Z ( dist ` G ) t ) )
26 1 22 2 16 18 17 19 21 25 tgcgrcomlr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Y ( dist ` G ) X ) = ( t ( dist ` G ) Z ) )
27 1 22 2 16 18 19 axtgcgrrflx 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( X ( dist ` G ) Z ) = ( Z ( dist ` G ) X ) )
28 eleq1w 
 |-  ( t = s -> ( t e. ( a I b ) <-> s e. ( a I b ) ) )
29 28 cbvrexvw 
 |-  ( E. t e. ( X L Z ) t e. ( a I b ) <-> E. s e. ( X L Z ) s e. ( a I b ) )
30 29 anbi2i 
 |-  ( ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) <-> ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. s e. ( X L Z ) s e. ( a I b ) ) )
31 30 opabbii 
 |-  { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. t e. ( X L Z ) t e. ( a I b ) ) } = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. s e. ( X L Z ) s e. ( a I b ) ) }
32 5 31 eqtri 
 |-  O = { <. a , b >. | ( ( a e. ( P \ ( X L Z ) ) /\ b e. ( P \ ( X L Z ) ) ) /\ E. s e. ( X L Z ) s e. ( a I b ) ) }
33 7 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> G e. TarskiGE )
34 1 2 3 6 8 10 14 tgelrnln 
 |-  ( ph -> ( X L Z ) e. ran L )
35 1 22 2 5 3 34 6 9 11 13 oppne1 
 |-  ( ph -> -. Y e. ( X L Z ) )
36 14 neneqd 
 |-  ( ph -> -. X = Z )
37 ioran 
 |-  ( -. ( Y e. ( X L Z ) \/ X = Z ) <-> ( -. Y e. ( X L Z ) /\ -. X = Z ) )
38 35 36 37 sylanbrc 
 |-  ( ph -> -. ( Y e. ( X L Z ) \/ X = Z ) )
39 1 3 2 6 8 10 9 38 ncolcom 
 |-  ( ph -> -. ( Y e. ( Z L X ) \/ Z = X ) )
40 1 3 2 6 10 8 9 39 ncolrot2 
 |-  ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
41 40 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
42 12 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( X L Y ) .|| ( Z L W ) )
43 simprl 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t ( ( hlG ` G ) ` Z ) W )
44 1 2 15 21 20 19 16 43 hlne1 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t =/= Z )
45 44 necomd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Z =/= t )
46 3 4 6 12 prlngrcl2 
 |-  ( ph -> ( Z L W ) e. ran L )
47 46 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Z L W ) e. ran L )
48 1 2 3 6 10 11 46 tglnne 
 |-  ( ph -> Z =/= W )
49 1 2 3 6 10 11 48 tglinerflx1 
 |-  ( ph -> Z e. ( Z L W ) )
50 49 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Z e. ( Z L W ) )
51 1 2 15 21 20 19 16 3 43 hlln 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t e. ( W L Z ) )
52 48 necomd 
 |-  ( ph -> W =/= Z )
53 1 2 3 6 11 10 52 tglinecom 
 |-  ( ph -> ( W L Z ) = ( Z L W ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( W L Z ) = ( Z L W ) )
55 51 54 eleqtrd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t e. ( Z L W ) )
56 1 2 3 16 19 21 45 45 47 50 55 tglinethru 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Z L W ) = ( Z L t ) )
57 42 56 breqtrd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( X L Y ) .|| ( Z L t ) )
58 34 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( X L Z ) e. ran L )
59 1 22 2 32 3 34 6 9 11 13 oppcom 
 |-  ( ph -> W O Y )
60 59 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> W O Y )
61 1 2 3 6 8 10 14 tglinerflx2 
 |-  ( ph -> Z e. ( X L Z ) )
62 61 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Z e. ( X L Z ) )
63 1 2 15 21 20 19 16 43 hlcomd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> W ( ( hlG ` G ) ` Z ) t )
64 1 22 2 32 3 58 16 15 20 21 17 60 62 63 opphl 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> t O Y )
65 1 22 2 32 3 58 16 21 17 64 oppcom 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> Y O t )
66 1 22 2 3 4 32 16 33 18 17 19 21 41 57 25 65 quadcgrprlng 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( ( Y L Z ) .|| ( t L X ) /\ ( Y ( dist ` G ) Z ) = ( t ( dist ` G ) X ) ) )
67 66 simprd 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Y ( dist ` G ) Z ) = ( t ( dist ` G ) X ) )
68 1 22 2 16 17 19 21 18 67 tgcgrcomlr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> ( Z ( dist ` G ) Y ) = ( X ( dist ` G ) t ) )
69 1 22 23 16 17 18 19 21 19 18 26 27 68 trgcgr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> <" Y X Z "> ( cgrG ` G ) <" t Z X "> )
70 1 2 15 8 8 10 6 14 hlid 
 |-  ( ph -> X ( ( hlG ` G ) ` Z ) X )
71 70 ad2antrr 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> X ( ( hlG ` G ) ` Z ) X )
72 1 2 15 16 17 18 19 20 19 18 21 18 69 43 71 iscgrad 
 |-  ( ( ( ph /\ t e. P ) /\ ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) ) -> <" Y X Z "> ( cgrA ` G ) <" W Z X "> )
73 3 4 6 12 prlngrcl1 
 |-  ( ph -> ( X L Y ) e. ran L )
74 1 2 3 6 8 9 73 tglnne 
 |-  ( ph -> X =/= Y )
75 1 2 15 10 8 9 6 11 22 52 74 hlcgrex 
 |-  ( ph -> E. t e. P ( t ( ( hlG ` G ) ` Z ) W /\ ( Z ( dist ` G ) t ) = ( X ( dist ` G ) Y ) ) )
76 72 75 r19.29a 
 |-  ( ph -> <" Y X Z "> ( cgrA ` G ) <" W Z X "> )