Metamath Proof Explorer


Theorem 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 φ G 𝒢 Tarski
iscgra.a φ A P
iscgra.b φ B P
iscgra.c φ C P
iscgra.d φ D P
iscgra.e φ E P
iscgra.f φ F P
iscgrad.x φ X P
iscgrad.y φ Y P
iscgrad.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEY ”⟩
iscgrad.2 φ X K E D
iscgrad.3 φ Y K E F
Assertion iscgrad φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩

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 φ G 𝒢 Tarski
5 iscgra.a φ A P
6 iscgra.b φ B P
7 iscgra.c φ C P
8 iscgra.d φ D P
9 iscgra.e φ E P
10 iscgra.f φ F P
11 iscgrad.x φ X P
12 iscgrad.y φ Y P
13 iscgrad.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEY ”⟩
14 iscgrad.2 φ X K E D
15 iscgrad.3 φ Y K E F
16 id x = X x = X
17 eqidd x = X E = E
18 eqidd x = X y = y
19 16 17 18 s3eqd x = X ⟨“ xEy ”⟩ = ⟨“ XEy ”⟩
20 19 breq2d x = X ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEy ”⟩
21 breq1 x = X x K E D X K E D
22 20 21 3anbi12d x = X ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEy ”⟩ X K E D y K E F
23 eqidd y = Y X = X
24 eqidd y = Y E = E
25 id y = Y y = Y
26 23 24 25 s3eqd y = Y ⟨“ XEy ”⟩ = ⟨“ XEY ”⟩
27 26 breq2d y = Y ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEy ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEY ”⟩
28 breq1 y = Y y K E F Y K E F
29 27 28 3anbi13d y = Y ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEy ”⟩ X K E D y K E F ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEY ”⟩ X K E D Y K E F
30 22 29 rspc2ev X P Y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ XEY ”⟩ X K E D Y K E F x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
31 11 12 13 14 15 30 syl113anc φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
32 1 2 3 4 5 6 7 8 9 10 iscgra φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
33 31 32 mpbird φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩