Metamath Proof Explorer


Theorem dfcgra2

Description: This is the full statement of definition 11.2 of Schwabhauser p. 95. This proof serves to confirm that the definition we have chosen, df-cgra is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses dfcgra2.p P = Base G
dfcgra2.i I = Itv G
dfcgra2.m - ˙ = dist G
dfcgra2.g φ G 𝒢 Tarski
dfcgra2.a φ A P
dfcgra2.b φ B P
dfcgra2.c φ C P
dfcgra2.d φ D P
dfcgra2.e φ E P
dfcgra2.f φ F P
Assertion dfcgra2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f

Proof

Step Hyp Ref Expression
1 dfcgra2.p P = Base G
2 dfcgra2.i I = Itv G
3 dfcgra2.m - ˙ = dist G
4 dfcgra2.g φ G 𝒢 Tarski
5 dfcgra2.a φ A P
6 dfcgra2.b φ B P
7 dfcgra2.c φ C P
8 dfcgra2.d φ D P
9 dfcgra2.e φ E P
10 dfcgra2.f φ F P
11 eqid hl 𝒢 G = hl 𝒢 G
12 4 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ G 𝒢 Tarski
13 5 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A P
14 6 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ B P
15 7 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ C P
16 8 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ D P
17 9 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ E P
18 10 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ F P
19 simpr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
20 1 2 11 12 13 14 15 16 17 18 19 cgrane1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A B
21 1 2 11 12 13 14 15 16 17 18 19 cgrane2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ B C
22 21 necomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ C B
23 20 22 jca φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A B C B
24 1 2 11 12 13 14 15 16 17 18 19 cgrane3 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ E D
25 24 necomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ D E
26 1 2 11 12 13 14 15 16 17 18 19 cgrane4 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ E F
27 26 necomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ F E
28 25 27 jca φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ D E F E
29 simprl φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F
30 simprr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
31 4 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C G 𝒢 Tarski
32 simp-5r φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a P
33 6 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B P
34 simp-4r φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c P
35 simpllr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C d P
36 9 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C E P
37 simplr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C f P
38 10 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C F P
39 8 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D P
40 7 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C P
41 5 ad6antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A P
42 simp-6r φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
43 1 2 31 11 41 33 40 39 36 38 42 cgracom φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ DEF ”⟩ 𝒢 G ⟨“ ABC ”⟩
44 29 simplld φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a
45 20 ad5antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B
46 1 3 2 31 33 41 32 44 45 tgbtwnne φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B a
47 1 2 11 33 32 41 31 41 44 46 45 btwnhl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A hl 𝒢 G B a
48 1 2 11 41 32 33 31 47 hlcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a hl 𝒢 G B A
49 1 2 11 31 39 36 38 41 33 40 43 32 48 cgrahl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ DEF ”⟩ 𝒢 G ⟨“ aBC ”⟩
50 29 simprld φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C B I c
51 22 ad5antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C B
52 1 3 2 31 33 40 34 50 51 tgbtwnne φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B c
53 1 2 11 33 34 40 31 41 50 52 51 btwnhl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C hl 𝒢 G B c
54 1 2 11 40 34 33 31 53 hlcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c hl 𝒢 G B C
55 1 2 11 31 39 36 38 32 33 40 49 34 54 cgrahl2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ DEF ”⟩ 𝒢 G ⟨“ aBc ”⟩
56 1 2 31 11 39 36 38 32 33 34 55 cgracom φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ aBc ”⟩ 𝒢 G ⟨“ DEF ”⟩
57 30 simplld φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D E I d
58 25 ad5antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D E
59 1 3 2 31 36 39 35 57 58 tgbtwnne φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C E d
60 1 2 11 36 35 39 31 41 57 59 58 btwnhl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D hl 𝒢 G E d
61 1 2 11 39 35 36 31 60 hlcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C d hl 𝒢 G E D
62 1 2 11 31 32 33 34 39 36 38 56 35 61 cgrahl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ aBc ”⟩ 𝒢 G ⟨“ dEF ”⟩
63 30 simprld φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C F E I f
64 27 ad5antr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C F E
65 1 3 2 31 36 38 37 63 64 tgbtwnne φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C E f
66 1 2 11 36 37 38 31 41 63 65 64 btwnhl1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C F hl 𝒢 G E f
67 1 2 11 38 37 36 31 66 hlcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C f hl 𝒢 G E F
68 1 2 11 31 32 33 34 35 36 38 62 37 67 cgrahl2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C ⟨“ aBc ”⟩ 𝒢 G ⟨“ dEf ”⟩
69 46 necomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a B
70 1 2 11 32 41 33 31 69 hlid φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a hl 𝒢 G B a
71 52 necomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c B
72 1 2 11 34 41 33 31 71 hlid φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c hl 𝒢 G B c
73 1 3 2 31 33 41 32 44 tgbtwncom φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A a I B
74 29 simplrd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A - ˙ a = E - ˙ D
75 1 3 2 31 41 32 36 39 74 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ A = E - ˙ D
76 30 simplrd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D - ˙ d = B - ˙ A
77 76 eqcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B - ˙ A = D - ˙ d
78 1 3 2 31 33 41 39 35 77 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A - ˙ B = D - ˙ d
79 1 3 2 31 32 41 33 36 39 35 73 57 75 78 tgcgrextend φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ B = E - ˙ d
80 1 3 2 31 32 33 36 35 79 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B - ˙ a = E - ˙ d
81 1 3 2 31 33 40 34 50 tgbtwncom φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C c I B
82 29 simprrd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C - ˙ c = E - ˙ F
83 1 3 2 31 40 34 36 38 82 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c - ˙ C = E - ˙ F
84 30 simprrd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C F - ˙ f = B - ˙ C
85 84 eqcomd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B - ˙ C = F - ˙ f
86 1 3 2 31 33 40 38 37 85 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C C - ˙ B = F - ˙ f
87 1 3 2 31 34 40 33 36 38 37 81 63 83 86 tgcgrextend φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C c - ˙ B = E - ˙ f
88 1 3 2 31 34 33 36 37 87 tgcgrcoml φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C B - ˙ c = E - ˙ f
89 1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88 cgracgr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
90 29 30 89 3jca φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
91 90 ex φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
92 91 reximdva φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
93 92 reximdva φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
94 93 imp φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
95 1 3 2 4 6 5 9 8 axtgsegcon φ a P A B I a A - ˙ a = E - ˙ D
96 1 3 2 4 6 7 9 10 axtgsegcon φ c P C B I c C - ˙ c = E - ˙ F
97 reeanv a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F a P A B I a A - ˙ a = E - ˙ D c P C B I c C - ˙ c = E - ˙ F
98 95 96 97 sylanbrc φ a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F
99 1 3 2 4 9 8 6 5 axtgsegcon φ d P D E I d D - ˙ d = B - ˙ A
100 1 3 2 4 9 10 6 7 axtgsegcon φ f P F E I f F - ˙ f = B - ˙ C
101 reeanv d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C d P D E I d D - ˙ d = B - ˙ A f P F E I f F - ˙ f = B - ˙ C
102 99 100 101 sylanbrc φ d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
103 98 102 jca φ a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
104 r19.41vv d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F
105 ancom D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
106 105 2rexbii d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
107 ancom d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
108 104 106 107 3bitr3i d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
109 108 2rexbii a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
110 r19.41vv a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
111 109 110 bitr2i a P c P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F d P f P D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
112 103 111 sylib φ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
113 112 adantr φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C
114 94 113 reximddv2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
115 23 28 114 3jca φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
116 df-3an A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
117 4 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t G 𝒢 Tarski
118 8 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D P
119 9 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t E P
120 10 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t F P
121 5 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A P
122 6 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B P
123 7 ad6antr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C P
124 simp-4r φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t y P
125 simp-5r φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t x P
126 simpllr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t z P
127 simplr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t t P
128 eqid 𝒢 G = 𝒢 G
129 simpr1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F
130 129 simplld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A B I x
131 simpr2 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C
132 131 simplld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D E I z
133 1 3 2 117 119 118 126 132 tgbtwncom φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D z I E
134 131 simplrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D - ˙ z = B - ˙ A
135 134 eqcomd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B - ˙ A = D - ˙ z
136 1 3 2 117 122 121 118 126 135 tgcgrcomr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B - ˙ A = z - ˙ D
137 129 simplrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A - ˙ x = E - ˙ D
138 1 3 2 117 121 125 119 118 137 tgcgrcomr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A - ˙ x = D - ˙ E
139 1 3 2 117 122 121 125 126 118 119 130 133 136 138 tgcgrextend φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B - ˙ x = z - ˙ E
140 1 3 2 117 122 125 126 119 139 tgcgrcoml φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t x - ˙ B = z - ˙ E
141 129 simprld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C B I y
142 1 3 2 117 122 123 124 141 tgbtwncom φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C y I B
143 131 simprld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t F E I t
144 129 simprrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C - ˙ y = E - ˙ F
145 1 3 2 117 123 124 119 120 144 tgcgrcoml φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t y - ˙ C = E - ˙ F
146 131 simprrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t F - ˙ t = B - ˙ C
147 146 eqcomd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B - ˙ C = F - ˙ t
148 1 3 2 117 122 123 120 127 147 tgcgrcoml φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C - ˙ B = F - ˙ t
149 1 3 2 117 124 123 122 119 120 127 142 143 145 148 tgcgrextend φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t y - ˙ B = E - ˙ t
150 1 3 2 117 124 122 119 127 149 tgcgrcoml φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B - ˙ y = E - ˙ t
151 simpr3 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t x - ˙ y = z - ˙ t
152 1 3 2 117 125 124 126 127 151 tgcgrcomlr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t y - ˙ x = t - ˙ z
153 1 3 128 117 125 122 124 126 119 127 140 150 152 trgcgr φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ xBy ”⟩ 𝒢 G ⟨“ zEt ”⟩
154 simp-6r φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A B C B D E F E
155 154 simprld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D E
156 1 3 2 117 119 118 126 132 155 tgbtwnne φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t E z
157 1 2 11 119 126 118 117 122 132 156 155 btwnhl1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t D hl 𝒢 G E z
158 1 2 11 118 126 119 117 157 hlcomd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t z hl 𝒢 G E D
159 154 simprrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t F E
160 1 3 2 117 119 120 127 143 159 tgbtwnne φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t E t
161 1 2 11 119 127 120 117 122 143 160 159 btwnhl1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t F hl 𝒢 G E t
162 1 2 11 120 127 119 117 161 hlcomd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t t hl 𝒢 G E F
163 1 2 11 117 125 122 124 118 119 120 126 127 153 158 162 iscgrad φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ xBy ”⟩ 𝒢 G ⟨“ DEF ”⟩
164 1 2 117 11 125 122 124 118 119 120 163 cgracom φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ DEF ”⟩ 𝒢 G ⟨“ xBy ”⟩
165 154 simplld φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A B
166 1 3 2 117 122 121 125 130 165 tgbtwnne φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B x
167 1 2 11 122 125 121 117 121 130 166 165 btwnhl1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t A hl 𝒢 G B x
168 1 2 11 117 118 119 120 125 122 124 164 121 167 cgrahl1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ DEF ”⟩ 𝒢 G ⟨“ ABy ”⟩
169 154 simplrd φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C B
170 1 3 2 117 122 123 124 141 169 tgbtwnne φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t B y
171 1 2 11 122 124 123 117 121 141 170 169 btwnhl1 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t C hl 𝒢 G B y
172 1 2 11 117 118 119 120 121 122 124 168 123 171 cgrahl2 φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ DEF ”⟩ 𝒢 G ⟨“ ABC ”⟩
173 1 2 117 11 118 119 120 121 122 123 172 cgracom φ A B C B D E F E x P y P z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
174 173 adantl3r φ A B C B D E F E x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
175 simpr φ A B C B D E F E x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f
176 oveq2 d = z E I d = E I z
177 176 eleq2d d = z D E I d D E I z
178 oveq2 d = z D - ˙ d = D - ˙ z
179 178 eqeq1d d = z D - ˙ d = B - ˙ A D - ˙ z = B - ˙ A
180 177 179 anbi12d d = z D E I d D - ˙ d = B - ˙ A D E I z D - ˙ z = B - ˙ A
181 180 anbi1d d = z D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C D E I z D - ˙ z = B - ˙ A F E I f F - ˙ f = B - ˙ C
182 oveq1 d = z d - ˙ f = z - ˙ f
183 182 eqeq2d d = z x - ˙ y = d - ˙ f x - ˙ y = z - ˙ f
184 181 183 3anbi23d d = z A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = z - ˙ f
185 oveq2 f = t E I f = E I t
186 185 eleq2d f = t F E I f F E I t
187 oveq2 f = t F - ˙ f = F - ˙ t
188 187 eqeq1d f = t F - ˙ f = B - ˙ C F - ˙ t = B - ˙ C
189 186 188 anbi12d f = t F E I f F - ˙ f = B - ˙ C F E I t F - ˙ t = B - ˙ C
190 189 anbi2d f = t D E I z D - ˙ z = B - ˙ A F E I f F - ˙ f = B - ˙ C D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C
191 oveq2 f = t z - ˙ f = z - ˙ t
192 191 eqeq2d f = t x - ˙ y = z - ˙ f x - ˙ y = z - ˙ t
193 190 192 3anbi23d f = t A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = z - ˙ f A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t
194 184 193 cbvrex2vw d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t
195 175 194 sylib φ A B C B D E F E x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f z P t P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I z D - ˙ z = B - ˙ A F E I t F - ˙ t = B - ˙ C x - ˙ y = z - ˙ t
196 174 195 r19.29vva φ A B C B D E F E x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
197 196 adantl3r φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
198 simpr φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f
199 oveq2 a = x B I a = B I x
200 199 eleq2d a = x A B I a A B I x
201 oveq2 a = x A - ˙ a = A - ˙ x
202 201 eqeq1d a = x A - ˙ a = E - ˙ D A - ˙ x = E - ˙ D
203 200 202 anbi12d a = x A B I a A - ˙ a = E - ˙ D A B I x A - ˙ x = E - ˙ D
204 203 anbi1d a = x A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F
205 oveq1 a = x a - ˙ c = x - ˙ c
206 205 eqeq1d a = x a - ˙ c = d - ˙ f x - ˙ c = d - ˙ f
207 204 206 3anbi13d a = x A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ c = d - ˙ f
208 207 2rexbidv a = x d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f d P f P A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ c = d - ˙ f
209 oveq2 c = y B I c = B I y
210 209 eleq2d c = y C B I c C B I y
211 oveq2 c = y C - ˙ c = C - ˙ y
212 211 eqeq1d c = y C - ˙ c = E - ˙ F C - ˙ y = E - ˙ F
213 210 212 anbi12d c = y C B I c C - ˙ c = E - ˙ F C B I y C - ˙ y = E - ˙ F
214 213 anbi2d c = y A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F
215 oveq2 c = y x - ˙ c = x - ˙ y
216 215 eqeq1d c = y x - ˙ c = d - ˙ f x - ˙ y = d - ˙ f
217 214 216 3anbi13d c = y A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ c = d - ˙ f A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f
218 217 2rexbidv c = y d P f P A B I x A - ˙ x = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ c = d - ˙ f d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f
219 208 218 cbvrex2vw a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f
220 198 219 sylib φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f x P y P d P f P A B I x A - ˙ x = E - ˙ D C B I y C - ˙ y = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C x - ˙ y = d - ˙ f
221 197 220 r19.29vva φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
222 221 anasss φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
223 116 222 sylan2b φ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
224 115 223 impbida φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ A B C B D E F E a P c P d P f P A B I a A - ˙ a = E - ˙ D C B I c C - ˙ c = E - ˙ F D E I d D - ˙ d = B - ˙ A F E I f F - ˙ f = B - ˙ C a - ˙ c = d - ˙ f