Metamath Proof Explorer


Theorem 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 φ G 𝒢 Tarski
cgraid.k K = hl 𝒢 G
cgraid.a φ A P
cgraid.b φ B P
cgraid.c φ C P
cgracom.d φ D P
cgracom.e φ E P
cgracom.f φ F P
cgracom.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
Assertion cgracom φ ⟨“ DEF ”⟩ 𝒢 G ⟨“ ABC ”⟩

Proof

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