cgrabtwn

Description: Angle congruence preserves flat angles. Part of Theorem 11.21 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	cgracol.p	$⊢ P = {Base}_{G}$
	cgracol.i	$⊢ I = Itv (G)$
	cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
	cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgracol.a	$⊢ φ \to A \in P$
	cgracol.b	$⊢ φ \to B \in P$
	cgracol.c	$⊢ φ \to C \in P$
	cgracol.d	$⊢ φ \to D \in P$
	cgracol.e	$⊢ φ \to E \in P$
	cgracol.f	$⊢ φ \to F \in P$
	cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgrabtwn.2	$⊢ φ \to B \in (A I C)$
Assertion	cgrabtwn	$⊢ φ \to E \in (D I F)$

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	$⊢ P = {Base}_{G}$
2		cgracol.i	$⊢ I = Itv (G)$
3		cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
4		cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgracol.a	$⊢ φ \to A \in P$
6		cgracol.b	$⊢ φ \to B \in P$
7		cgracol.c	$⊢ φ \to C \in P$
8		cgracol.d	$⊢ φ \to D \in P$
9		cgracol.e	$⊢ φ \to E \in P$
10		cgracol.f	$⊢ φ \to F \in P$
11		cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgrabtwn.2	$⊢ φ \to B \in (A I C)$
13		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
14		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to x \in P$
15	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to D \in P$
16	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to F \in P$
17	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to G \in 𝒢_{Tarski}$
18	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in P$
19		simpr2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to x {hl}_{𝒢} (G) (E) D$
20		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to y \in P$
21		simpr3	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to y {hl}_{𝒢} (G) (E) F$
22		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
23	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to A \in P$
24	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to B \in P$
25	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to C \in P$
26		simpr1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
27	12	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to B \in (A I C)$
28	1 3 2 22 17 23 24 25 14 18 20 26 27	tgbtwnxfr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (x I y)$
29	1 3 2 17 14 18 20 28	tgbtwncom	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (y I x)$
30	1 2 13 20 16 14 17 18 21 29	btwnhl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (F I x)$
31	1 3 2 17 16 18 14 30	tgbtwncom	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (x I F)$
32	1 2 13 14 15 16 17 18 19 31	btwnhl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (D I F)$
33	1 2 13 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 {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F))$
34	11 33	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)$
35	32 34	r19.29vva	$⊢ φ \to E \in (D I F)$

Metamath Proof Explorer

Theorem cgrabtwn

Proof