cgrahl

Description: Angle congruence preserves null 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 ”⟩$
	cgrahl.k	$⊢ K = {hl}_{𝒢} (G)$
	cgrahl.2	$⊢ φ \to A K (B) C$
Assertion	cgrahl	$⊢ φ \to D K (E) 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		cgrahl.k	$⊢ K = {hl}_{𝒢} (G)$
13		cgrahl.2	$⊢ φ \to A K (B) C$
14	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$
15		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$
16	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$
17	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}$
18	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$
19		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$
20		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$
21	1 2 12 19 14 18 17 20	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 D K (E) x$
22	1 2 12 19 14 18 17 20	hlne1	$⊢ (((φ \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 \neq E$
23		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$
24	1 2 12 15 16 18 17 23	hlne1	$⊢ (((φ \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 \neq E$
25		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
26	17	adantr	$⊢ ((((φ \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)) \land A \in (B I C)) \to G \in 𝒢_{Tarski}$
27	6	ad4antr	$⊢ ((((φ \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)) \land A \in (B I C)) \to B \in P$
28	5	ad4antr	$⊢ ((((φ \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)) \land A \in (B I C)) \to A \in P$
29	7	ad4antr	$⊢ ((((φ \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)) \land A \in (B I C)) \to C \in P$
30	18	adantr	$⊢ ((((φ \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)) \land A \in (B I C)) \to E \in P$
31	19	adantr	$⊢ ((((φ \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)) \land A \in (B I C)) \to x \in P$
32		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)) \land A \in (B I C)) \to y \in P$
33		simplr1	$⊢ ((((φ \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)) \land A \in (B I C)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
34	1 3 2 25 26 28 27 29 31 30 32 33	cgr3swap12	$⊢ ((((φ \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)) \land A \in (B I C)) \to ⟨“ B A C ”⟩ \sim_{𝒢} (G) ⟨“ E x y ”⟩$
35		simpr	$⊢ ((((φ \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)) \land A \in (B I C)) \to A \in (B I C)$
36	1 3 2 25 26 27 28 29 30 31 32 34 35	tgbtwnxfr	$⊢ ((((φ \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)) \land A \in (B I C)) \to x \in (E I y)$
37	36	orcd	$⊢ ((((φ \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)) \land A \in (B I C)) \to (x \in (E I y) \lor y \in (E I x))$
38	4	ad4antr	$⊢ ((((φ \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)) \land C \in (B I A)) \to G \in 𝒢_{Tarski}$
39	6	ad4antr	$⊢ ((((φ \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)) \land C \in (B I A)) \to B \in P$
40	7	ad4antr	$⊢ ((((φ \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)) \land C \in (B I A)) \to C \in P$
41	5	ad4antr	$⊢ ((((φ \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)) \land C \in (B I A)) \to A \in P$
42	9	ad4antr	$⊢ ((((φ \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)) \land C \in (B I A)) \to E \in P$
43		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)) \land C \in (B I A)) \to y \in P$
44	19	adantr	$⊢ ((((φ \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)) \land C \in (B I A)) \to x \in P$
45		simplr1	$⊢ ((((φ \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)) \land C \in (B I A)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
46	1 3 2 25 38 41 39 40 44 42 43 45	cgr3rotl	$⊢ ((((φ \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)) \land C \in (B I A)) \to ⟨“ B C A ”⟩ \sim_{𝒢} (G) ⟨“ E y x ”⟩$
47		simpr	$⊢ ((((φ \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)) \land C \in (B I A)) \to C \in (B I A)$
48	1 3 2 25 38 39 40 41 42 43 44 46 47	tgbtwnxfr	$⊢ ((((φ \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)) \land C \in (B I A)) \to y \in (E I x)$
49	48	olcd	$⊢ ((((φ \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)) \land C \in (B I A)) \to (x \in (E I y) \lor y \in (E I x))$
50	1 2 12 5 7 6 4	ishlg	$⊢ φ \to (A K (B) C \leftrightarrow (A \neq B \land C \neq B \land (A \in (B I C) \lor C \in (B I A))))$
51	13 50	mpbid	$⊢ φ \to (A \neq B \land C \neq B \land (A \in (B I C) \lor C \in (B I A)))$
52	51	simp3d	$⊢ φ \to (A \in (B I C) \lor C \in (B I A))$
53	52	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 (B I C) \lor C \in (B I A))$
54	37 49 53	mpjaodan	$⊢ (((φ \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 (E I y) \lor y \in (E I x))$
55	1 2 12 19 15 18 17	ishlg	$⊢ (((φ \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) y \leftrightarrow (x \neq E \land y \neq E \land (x \in (E I y) \lor y \in (E I x))))$
56	22 24 54 55	mpbir3and	$⊢ (((φ \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) y$
57	1 2 12 14 19 15 17 18 21 56	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 D K (E) y$
58	1 2 12 14 15 16 17 18 57 23	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 D K (E) F$
59	1 2 12 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))$
60	11 59	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)$
61	58 60	r19.29vva	$⊢ φ \to D K (E) F$

Metamath Proof Explorer

Theorem cgrahl

Proof