iscgrad

Description: Sufficient conditions for angle congruence, deduction version. (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$
	iscgrad.x	$⊢ φ \to X \in P$
	iscgrad.y	$⊢ φ \to Y \in P$
	iscgrad.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Y ”⟩$
	iscgrad.2	$⊢ φ \to X K (E) D$
	iscgrad.3	$⊢ φ \to Y K (E) F$
Assertion	iscgrad	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

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		iscgrad.x	$⊢ φ \to X \in P$
12		iscgrad.y	$⊢ φ \to Y \in P$
13		iscgrad.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Y ”⟩$
14		iscgrad.2	$⊢ φ \to X K (E) D$
15		iscgrad.3	$⊢ φ \to Y K (E) F$
16		id	$⊢ x = X \to x = X$
17		eqidd	$⊢ x = X \to E = E$
18		eqidd	$⊢ x = X \to y = y$
19	16 17 18	s3eqd	$⊢ x = X \to ⟨“ x E y ”⟩ = ⟨“ X E y ”⟩$
20	19	breq2d	$⊢ x = X \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩)$
21		breq1	$⊢ x = X \to (x K (E) D \leftrightarrow X K (E) D)$
22	20 21	3anbi12d	$⊢ x = X \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩ \land X K (E) D \land y K (E) F))$
23		eqidd	$⊢ y = Y \to X = X$
24		eqidd	$⊢ y = Y \to E = E$
25		id	$⊢ y = Y \to y = Y$
26	23 24 25	s3eqd	$⊢ y = Y \to ⟨“ X E y ”⟩ = ⟨“ X E Y ”⟩$
27	26	breq2d	$⊢ y = Y \to (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩ \leftrightarrow ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Y ”⟩)$
28		breq1	$⊢ y = Y \to (y K (E) F \leftrightarrow Y K (E) F)$
29	27 28	3anbi13d	$⊢ y = Y \to ((⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E y ”⟩ \land X K (E) D \land y K (E) F) \leftrightarrow (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ X E Y ”⟩ \land X K (E) D \land Y K (E) F))$
30	22 29	rspc2ev	$⊢ (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 \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)$
31	11 12 13 14 15 30	syl113anc	$⊢ φ \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)$
32	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))$
33	31 32	mpbird	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem iscgrad

Proof