tgaas1

Description: Under the AAS hypotheses, the side included between the two given angles is congruent. This is the whole content of AAS: tgaas simply packages it with SAS ( tgsas ). The point copied onto ray E F by tgaascgra is eliminated here. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		tgaas1.p	$⊢ P = {Base}_{G}$
2		tgaas1.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgaas1.i	$⊢ I = Itv (G)$
4		tgaas1.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgaas1.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgaas1.a	$⊢ φ \to A \in P$
7		tgaas1.b	$⊢ φ \to B \in P$
8		tgaas1.c	$⊢ φ \to C \in P$
9		tgaas1.d	$⊢ φ \to D \in P$
10		tgaas1.e	$⊢ φ \to E \in P$
11		tgaas1.f	$⊢ φ \to F \in P$
12		tgaas1.ncol	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
13		tgaas1.1	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
14		tgaas1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
15		tgaas1.3	$⊢ φ \to ⟨“ B C A ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E F D ”⟩$
16		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
17	5	adantr	$⊢ (φ \land x \in P) \to G \in 𝒢_{Tarski}$
18	17	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
19	6	adantr	$⊢ (φ \land x \in P) \to A \in P$
20	19	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \in P$
21	7	adantr	$⊢ (φ \land x \in P) \to B \in P$
22	21	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to B \in P$
23	8	adantr	$⊢ (φ \land x \in P) \to C \in P$
24	23	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to C \in P$
25	9	adantr	$⊢ (φ \land x \in P) \to D \in P$
26	25	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to D \in P$
27	10	adantr	$⊢ (φ \land x \in P) \to E \in P$
28	27	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to E \in P$
29	11	adantr	$⊢ (φ \land x \in P) \to F \in P$
30	29	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to F \in P$
31		simpl	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to (φ \land x \in P)$
32	31	simprd	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to x \in P$
33	12	adantr	$⊢ (φ \land x \in P) \to \neg (C \in (A L B) \lor A = B)$
34	33	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to \neg (C \in (A L B) \lor A = B)$
35	13	adantr	$⊢ (φ \land x \in P) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
36	35	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to A \underset{˙}{-} B = D \underset{˙}{-} E$
37	14	adantr	$⊢ (φ \land x \in P) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
38	37	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
39	15	adantr	$⊢ (φ \land x \in P) \to ⟨“ B C A ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E F D ”⟩$
40	39	adantr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to ⟨“ B C A ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E F D ”⟩$
41		simpr	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)$
42	41	simpld	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to x {hl}_{𝒢} (G) (E) F$
43	41	simprd	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to E \underset{˙}{-} x = B \underset{˙}{-} C$
44	1 2 3 4 16 18 20 22 24 26 28 30 32 34 36 38 40 42 43	tgaas1h	$⊢ ((φ \land x \in P) \land (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)) \to B \underset{˙}{-} C = E \underset{˙}{-} F$
45	1 3 2 5 6 7 8 9 10 11 14 4 12	cgrancol	$⊢ φ \to \neg (F \in (D L E) \lor D = E)$
46	1 3 4 5 9 10 11 45	tgbcne	$⊢ φ \to E \neq F$
47	46	necomd	$⊢ φ \to F \neq E$
48	1 3 4 5 6 7 8 12	tgbcne	$⊢ φ \to B \neq C$
49	1 3 16 10 7 8 5 11 2 47 48	hlcgrex	$⊢ φ \to \exists x \in P (x {hl}_{𝒢} (G) (E) F \land E \underset{˙}{-} x = B \underset{˙}{-} C)$
50	44 49	r19.29a	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$

Metamath Proof Explorer

Theorem tgaas1

Proof