Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaas1.m ⊢ − = ( dist ‘ 𝐺 )
tgaas1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaas1.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaas1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaas1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgaas1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgaas1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgaas1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgaas1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgaas1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgaas1.ncol ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
tgaas1.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
tgaas1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
tgaas1.3 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
Assertion tgaas1 ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tgaas1.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaas1.m ⊢ − = ( dist ‘ 𝐺 )
3 tgaas1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgaas1.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgaas1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgaas1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgaas1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgaas1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgaas1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgaas1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 tgaas1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 tgaas1.ncol ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
13 tgaas1.1 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
14 tgaas1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
15 tgaas1.3 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
16 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐴 ∈ 𝑃 )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∈ 𝑃 )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐵 ∈ 𝑃 )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ 𝑃 )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐶 ∈ 𝑃 )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
25 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐷 ∈ 𝑃 )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ 𝑃 )
27 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐸 ∈ 𝑃 )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐸 ∈ 𝑃 )
29 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → 𝐹 ∈ 𝑃 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ∈ 𝑃 )
31 simpl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) )
32 31 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 ∈ 𝑃 )
33 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
35 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
37 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
39 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
41 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) )
42 41 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
43 41 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) )
44 1 2 3 4 16 18 20 22 24 26 28 30 32 34 36 38 40 42 43 tgaas1h ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
45 1 3 2 5 6 7 8 9 10 11 14 4 12 cgrancol ⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
46 1 3 4 5 9 10 11 45 tgbcne ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
47 46 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
48 1 3 4 5 6 7 8 12 tgbcne ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
49 1 3 16 10 7 8 5 11 2 47 48 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐶 ) ) )
50 44 49 r19.29a ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )