cgracom

Description: Angle congruence commutes. Theorem 11.7 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		cgraid.p	$⊢ P = {Base}_{G}$
2		cgraid.i	$⊢ I = Itv (G)$
3		cgraid.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		cgraid.k	$⊢ K = {hl}_{𝒢} (G)$
5		cgraid.a	$⊢ φ \to A \in P$
6		cgraid.b	$⊢ φ \to B \in P$
7		cgraid.c	$⊢ φ \to C \in P$
8		cgracom.d	$⊢ φ \to D \in P$
9		cgracom.e	$⊢ φ \to E \in P$
10		cgracom.f	$⊢ φ \to F \in P$
11		cgracom.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		eqid	$⊢ dist (G) = dist (G)$
13		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
14	3	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to G \in 𝒢_{Tarski}$
15	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to D \in P$
16	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to E \in P$
17	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to F \in P$
18		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to x \in P$
19	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to B \in P$
20		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to y \in P$
21		simprlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to B dist (G) x = E dist (G) D$
22	21	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to E dist (G) D = B dist (G) x$
23	1 12 2 14 16 15 19 18 22	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to D dist (G) E = x dist (G) B$
24		simprrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to B dist (G) y = E dist (G) F$
25	24	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to E dist (G) F = B dist (G) y$
26	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to A \in P$
27	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to C \in P$
28	11	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
29		simprll	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to x K (B) A$
30		simprrl	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to y K (B) C$
31	1 2 4 14 26 19 27 15 16 17 28 18 12 20 29 30 21 24	cgracgr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to x dist (G) y = D dist (G) F$
32	31	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to D dist (G) F = x dist (G) y$
33	1 12 2 14 15 17 18 20 32	tgcgrcomlr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to F dist (G) D = y dist (G) x$
34	1 12 13 14 15 16 17 18 19 20 23 25 33	trgcgr	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to ⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x B y ”⟩$
35	34 29 30	3jca	$⊢ (((φ \land x \in P) \land y \in P) \land ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))) \to (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x B y ”⟩ \land x K (B) A \land y K (B) C)$
36	1 2 4 3 5 6 7 8 9 10 11	cgrane1	$⊢ φ \to A \neq B$
37	1 2 4 3 5 6 7 8 9 10 11	cgrane3	$⊢ φ \to E \neq D$
38	1 2 4 6 9 8 3 5 12 36 37	hlcgrex	$⊢ φ \to \exists x \in P (x K (B) A \land B dist (G) x = E dist (G) D)$
39	1 2 4 3 5 6 7 8 9 10 11	cgrane2	$⊢ φ \to B \neq C$
40	39	necomd	$⊢ φ \to C \neq B$
41	1 2 4 3 5 6 7 8 9 10 11	cgrane4	$⊢ φ \to E \neq F$
42	1 2 4 6 9 10 3 7 12 40 41	hlcgrex	$⊢ φ \to \exists y \in P (y K (B) C \land B dist (G) y = E dist (G) F)$
43		reeanv	$⊢ \exists x \in P \exists y \in P ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F)) \leftrightarrow (\exists x \in P (x K (B) A \land B dist (G) x = E dist (G) D) \land \exists y \in P (y K (B) C \land B dist (G) y = E dist (G) F))$
44	38 42 43	sylanbrc	$⊢ φ \to \exists x \in P \exists y \in P ((x K (B) A \land B dist (G) x = E dist (G) D) \land (y K (B) C \land B dist (G) y = E dist (G) F))$
45	35 44	reximddv2	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x B y ”⟩ \land x K (B) A \land y K (B) C)$
46	1 2 4 3 8 9 10 5 6 7	iscgra	$⊢ φ \to (⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x B y ”⟩ \land x K (B) A \land y K (B) C))$
47	45 46	mpbird	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$

Metamath Proof Explorer

Theorem cgracom

Proof