cgrahl2

Description: Angle congruence is independent of the choice of points on the rays. Proposition 11.10 of Schwabhauser p. 95. (Contributed by Thierry Arnoux, 1-Aug-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
	cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgrahl1.x	$⊢ φ \to X \in P$
	cgrahl2.1	$⊢ φ \to X K (E) F$
Assertion	cgrahl2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E X ”⟩$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgrahl1.x	$⊢ φ \to X \in P$
13		cgrahl2.1	$⊢ φ \to X K (E) F$
14	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to G \in 𝒢_{Tarski}$
15	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \in P$
16	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \in P$
17	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \in P$
18	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to D \in P$
19	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \in P$
20	12	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to X \in P$
21		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \in P$
22		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y \in P$
23		simpr1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
24		simpr2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x K (E) D$
25	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to F \in P$
26		simpr3	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y K (E) F$
27	13	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to X K (E) F$
28	1 2 3 20 25 19 14 27	hlcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to F K (E) X$
29	1 2 3 22 25 20 14 19 26 28	hltr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y K (E) X$
30	1 2 3 14 15 16 17 18 19 20 21 22 23 24 29	iscgrad	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E X ”⟩$
31	1 2 3 4 5 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
32	11 31	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)$
33	30 32	r19.29vva	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E X ”⟩$

Metamath Proof Explorer

Theorem cgrahl2

Proof