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 = {Line}_{𝒢} (G)$
	tgaltai.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	tgaltai.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
	tgaltai.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaltai.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	tgaltai.x	$⊢ φ \to X \in P$
	tgaltai.y	$⊢ φ \to Y \in P$
	tgaltai.z	$⊢ φ \to Z \in P$
	tgaltai.w	$⊢ φ \to W \in P$
	tgaltai.2	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
	tgaltai.3	$⊢ φ \to Y O W$
	tgaltai.4	$⊢ φ \to X \neq Z$
Assertion	tgaltai	$⊢ φ \to ⟨“ Y X Z ”⟩ \sim_{𝒢}^{∠} (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 = {Line}_{𝒢} (G)$
4		tgaltai.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
5		tgaltai.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
6		tgaltai.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		tgaltai.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		tgaltai.x	$⊢ φ \to X \in P$
9		tgaltai.y	$⊢ φ \to Y \in P$
10		tgaltai.z	$⊢ φ \to Z \in P$
11		tgaltai.w	$⊢ φ \to W \in P$
12		tgaltai.2	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
13		tgaltai.3	$⊢ φ \to Y O W$
14		tgaltai.4	$⊢ φ \to X \neq Z$
15		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
16	6	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to G \in 𝒢_{Tarski}$
17	9	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Y \in P$
18	8	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to X \in P$
19	10	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z \in P$
20	11	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to W \in P$
21		simplr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t \in P$
22		eqid	$⊢ dist (G) = dist (G)$
23		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
24		simprr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z dist (G) t = X dist (G) Y$
25	24	eqcomd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to X dist (G) Y = Z dist (G) t$
26	1 22 2 16 18 17 19 21 25	tgcgrcomlr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Y dist (G) X = t dist (G) Z$
27	1 22 2 16 18 19	axtgcgrrflx	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to X dist (G) Z = Z dist (G) X$
28		eleq1w	$⊢ t = s \to (t \in (a I b) \leftrightarrow s \in (a I b))$
29	28	cbvrexvw	$⊢ \exists t \in (X L Z) t \in (a I b) \leftrightarrow \exists s \in (X L Z) s \in (a I b)$
30	29	anbi2i	$⊢ ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b)) \leftrightarrow ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists s \in (X L Z) s \in (a I b))$
31	30	opabbii	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\} = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists s \in (X L Z) s \in (a I b))\}$
32	5 31	eqtri	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists s \in (X L Z) s \in (a I b))\}$
33	7	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to G \in 𝒢_{Tarski}^{E}$
34	1 2 3 6 8 10 14	tgelrnln	$⊢ φ \to X L Z \in ran L$
35	1 22 2 5 3 34 6 9 11 13	oppne1	$⊢ φ \to \neg Y \in (X L Z)$
36	14	neneqd	$⊢ φ \to \neg X = Z$
37		ioran	$⊢ \neg (Y \in (X L Z) \lor X = Z) \leftrightarrow (\neg Y \in (X L Z) \land \neg X = Z)$
38	35 36 37	sylanbrc	$⊢ φ \to \neg (Y \in (X L Z) \lor X = Z)$
39	1 3 2 6 8 10 9 38	ncolcom	$⊢ φ \to \neg (Y \in (Z L X) \lor Z = X)$
40	1 3 2 6 10 8 9 39	ncolrot2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
41	40	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to \neg (X \in (Y L Z) \lor Y = Z)$
42	12	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to (X L Y) \underset{˙}{∥} (Z L W)$
43		simprl	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t {hl}_{𝒢} (G) (Z) W$
44	1 2 15 21 20 19 16 43	hlne1	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t \neq Z$
45	44	necomd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z \neq t$
46	3 4 6 12	prlngrcl2	$⊢ φ \to Z L W \in ran L$
47	46	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z L W \in ran L$
48	1 2 3 6 10 11 46	tglnne	$⊢ φ \to Z \neq W$
49	1 2 3 6 10 11 48	tglinerflx1	$⊢ φ \to Z \in (Z L W)$
50	49	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z \in (Z L W)$
51	1 2 15 21 20 19 16 3 43	hlln	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t \in (W L Z)$
52	48	necomd	$⊢ φ \to W \neq Z$
53	1 2 3 6 11 10 52	tglinecom	$⊢ φ \to W L Z = Z L W$
54	53	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to W L Z = Z L W$
55	51 54	eleqtrd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t \in (Z L W)$
56	1 2 3 16 19 21 45 45 47 50 55	tglinethru	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z L W = Z L t$
57	42 56	breqtrd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to (X L Y) \underset{˙}{∥} (Z L t)$
58	34	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to X L Z \in ran L$
59	1 22 2 32 3 34 6 9 11 13	oppcom	$⊢ φ \to W O Y$
60	59	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to W O Y$
61	1 2 3 6 8 10 14	tglinerflx2	$⊢ φ \to Z \in (X L Z)$
62	61	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z \in (X L Z)$
63	1 2 15 21 20 19 16 43	hlcomd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to W {hl}_{𝒢} (G) (Z) t$
64	1 22 2 32 3 58 16 15 20 21 17 60 62 63	opphl	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to t O Y$
65	1 22 2 32 3 58 16 21 17 64	oppcom	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Y O t$
66	1 22 2 3 4 32 16 33 18 17 19 21 41 57 25 65	quadcgrprlng	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to ((Y L Z) \underset{˙}{∥} (t L X) \land Y dist (G) Z = t dist (G) X)$
67	66	simprd	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Y dist (G) Z = t dist (G) X$
68	1 22 2 16 17 19 21 18 67	tgcgrcomlr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to Z dist (G) Y = X dist (G) t$
69	1 22 23 16 17 18 19 21 19 18 26 27 68	trgcgr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to ⟨“ Y X Z ”⟩ \sim_{𝒢} (G) ⟨“ t Z X ”⟩$
70	1 2 15 8 8 10 6 14	hlid	$⊢ φ \to X {hl}_{𝒢} (G) (Z) X$
71	70	ad2antrr	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to X {hl}_{𝒢} (G) (Z) X$
72	1 2 15 16 17 18 19 20 19 18 21 18 69 43 71	iscgrad	$⊢ ((φ \land t \in P) \land (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)) \to ⟨“ Y X Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ W Z X ”⟩$
73	3 4 6 12	prlngrcl1	$⊢ φ \to X L Y \in ran L$
74	1 2 3 6 8 9 73	tglnne	$⊢ φ \to X \neq Y$
75	1 2 15 10 8 9 6 11 22 52 74	hlcgrex	$⊢ φ \to \exists t \in P (t {hl}_{𝒢} (G) (Z) W \land Z dist (G) t = X dist (G) Y)$
76	72 75	r19.29a	$⊢ φ \to ⟨“ Y X Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ W Z X ”⟩$

Metamath Proof Explorer

Theorem tgaltai

Proof