Metamath Proof Explorer


Theorem angmndaddcpbl

Description: Addition of angles is compatible with angle congruence. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmndadd.p P = Base G
angmndadd.a A = d P 0 ..^ 3 | d 0 d 1 d 1 d 2
angmndadd.i I = Itv G
angmndadd.d - ˙ = dist G
angmndadd.c ˙ = 𝒢 G
angmndadd.l L = Line 𝒢 G
angmndadd.g φ G 𝒢 Tarski
angmndadd.o + ˙ = e A , f A if e 0 e 1 L e 2 ⟨“ f 0 f 1 ι s P | ⟨“ f 2 f 1 s ”⟩ ˙ e f 1 - ˙ s = e 1 - ˙ e 0 ”⟩ ⟨“ e 0 e 1 ι s P | ⟨“ e 2 e 1 s ”⟩ ˙ f e 1 - ˙ s = f 1 - ˙ f 0 e 1 L e 2 s I e 0 ”⟩
angmndaddcpbl.c φ C A
angmndaddcpbl.d φ D A
angmndaddcpbl.e φ E A
angmndaddcpbl.f φ F A
angmndaddcpbl.2 φ E ˙ C
angmndaddcpbl.3 φ F ˙ D
Assertion angmndaddcpbl φ E + ˙ F ˙ C + ˙ D

Proof

Step Hyp Ref Expression
1 angmndadd.p P = Base G
2 angmndadd.a A = d P 0 ..^ 3 | d 0 d 1 d 1 d 2
3 angmndadd.i I = Itv G
4 angmndadd.d - ˙ = dist G
5 angmndadd.c ˙ = 𝒢 G
6 angmndadd.l L = Line 𝒢 G
7 angmndadd.g φ G 𝒢 Tarski
8 angmndadd.o + ˙ = e A , f A if e 0 e 1 L e 2 ⟨“ f 0 f 1 ι s P | ⟨“ f 2 f 1 s ”⟩ ˙ e f 1 - ˙ s = e 1 - ˙ e 0 ”⟩ ⟨“ e 0 e 1 ι s P | ⟨“ e 2 e 1 s ”⟩ ˙ f e 1 - ˙ s = f 1 - ˙ f 0 e 1 L e 2 s I e 0 ”⟩
9 angmndaddcpbl.c φ C A
10 angmndaddcpbl.d φ D A
11 angmndaddcpbl.e φ E A
12 angmndaddcpbl.f φ F A
13 angmndaddcpbl.2 φ E ˙ C
14 angmndaddcpbl.3 φ F ˙ D
15 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P E = ⟨“ xyz ”⟩
16 15 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x E = ⟨“ xyz ”⟩
17 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x F = ⟨“ uvw ”⟩
18 16 17 oveq12d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x E + ˙ F = ⟨“ xyz ”⟩ + ˙ ⟨“ uvw ”⟩
19 7 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c G 𝒢 Tarski
20 19 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k G 𝒢 Tarski
21 20 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z G 𝒢 Tarski
22 21 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z G 𝒢 Tarski
23 22 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x G 𝒢 Tarski
24 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z u P
25 24 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x u P
26 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z v P
27 26 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x v P
28 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z w P
29 28 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x w P
30 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z x P
31 30 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z x P
32 31 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x x P
33 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z y P
34 33 adantr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P y P
35 34 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z y P
36 35 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x y P
37 simp-11r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z z P
38 37 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x z P
39 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z u v
40 39 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x u v
41 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z v w
42 41 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x v w
43 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z x y
44 43 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x x y
45 simp-8r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z y z
46 45 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x y z
47 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z x y L z
48 47 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x x y L z
49 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x t P
50 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩
51 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x v - ˙ t = y - ˙ x
52 1 2 3 4 5 6 23 25 27 29 32 36 38 40 42 44 46 8 48 49 50 51 angmndaddov2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x ⟨“ xyz ”⟩ + ˙ ⟨“ uvw ”⟩ = ⟨“ uvt ”⟩
53 18 52 eqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x E + ˙ F = ⟨“ uvt ”⟩
54 23 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a G 𝒢 Tarski
55 29 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a w P
56 simp-10r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z k P
57 56 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x k P
58 57 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a k P
59 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k i P
60 59 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z i P
61 60 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x i P
62 61 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a i P
63 simp-11r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z j P
64 63 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x j P
65 64 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a j P
66 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h P
67 25 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a u P
68 27 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a v P
69 49 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t P
70 42 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a v w
71 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z j k
72 71 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x j k
73 72 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a j k
74 32 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a x P
75 36 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a y P
76 38 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a z P
77 eqid hl 𝒢 G = hl 𝒢 G
78 5 a1i φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ˙ = 𝒢 G
79 50 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩
80 78 79 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ wvt ”⟩ 𝒢 G ⟨“ xyz ”⟩
81 1 3 54 77 55 68 69 74 75 76 80 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ xyz ”⟩ 𝒢 G ⟨“ wvt ”⟩
82 1 3 6 22 31 35 37 43 47 45 lnrot2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z z x L y
83 82 orcd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z z x L y x = y
84 83 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a z x L y x = y
85 1 3 4 54 74 75 76 55 68 69 81 6 84 cgracol φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t w L v w = v
86 70 necomd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a w v
87 86 neneqd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ¬ w = v
88 85 87 olcnd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t w L v
89 1 3 6 54 68 55 69 70 88 lncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t v L w
90 1 4 3 54 67 69 tgbtwntriv2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t u I t
91 89 90 elind φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a t v L w u I t
92 91 ne0d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a v L w u I t
93 simp-11r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j a P
94 93 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z a P
95 94 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x a P
96 95 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a a P
97 simp-10r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j b P
98 97 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z b P
99 98 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x b P
100 99 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a b P
101 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j c P
102 101 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z c P
103 102 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x c P
104 103 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a c P
105 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩
106 78 105 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ kjh ”⟩ 𝒢 G ⟨“ abc ”⟩
107 1 3 54 77 58 65 66 96 100 104 106 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ abc ”⟩ 𝒢 G ⟨“ kjh ”⟩
108 94 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z a P
109 98 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z b P
110 102 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z c P
111 5 a1i φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z ˙ = 𝒢 G
112 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E = ⟨“ xyz ”⟩
113 13 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c E ˙ C
114 113 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k E ˙ C
115 114 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E ˙ C
116 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k C = ⟨“ abc ”⟩
117 116 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z C = ⟨“ abc ”⟩
118 115 117 breqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E ˙ ⟨“ abc ”⟩
119 112 118 eqbrtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z ⟨“ xyz ”⟩ ˙ ⟨“ abc ”⟩
120 111 119 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z ⟨“ xyz ”⟩ 𝒢 G ⟨“ abc ”⟩
121 120 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z ⟨“ xyz ”⟩ 𝒢 G ⟨“ abc ”⟩
122 1 3 4 22 31 35 37 108 109 110 121 6 83 cgracol φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z c a L b a = b
123 122 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a c a L b a = b
124 1 3 4 54 96 100 104 58 65 66 107 6 123 cgracol φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h k L j k = j
125 73 necomd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a k j
126 125 neneqd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ¬ k = j
127 124 126 olcnd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h k L j
128 1 3 6 54 65 58 66 73 127 lncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h j L k
129 1 4 3 54 62 66 tgbtwntriv2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h i I h
130 128 129 elind φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h j L k i I h
131 130 ne0d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a j L k i I h
132 17 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a F = ⟨“ uvw ”⟩
133 14 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c F ˙ D
134 133 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k F ˙ D
135 134 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z F ˙ D
136 135 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x F ˙ D
137 136 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a F ˙ D
138 132 137 eqbrtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ uvw ”⟩ ˙ D
139 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z D = ⟨“ ijk ”⟩
140 139 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z D = ⟨“ ijk ”⟩
141 140 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a D = ⟨“ ijk ”⟩
142 138 141 breqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ uvw ”⟩ ˙ ⟨“ ijk ”⟩
143 5 eqcomi 𝒢 G = ˙
144 143 a1i φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a 𝒢 G = ˙
145 121 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ xyz ”⟩ 𝒢 G ⟨“ abc ”⟩
146 1 3 54 77 74 75 76 96 100 104 145 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ abc ”⟩ 𝒢 G ⟨“ xyz ”⟩
147 1 3 54 77 58 65 66 96 100 104 106 74 75 76 146 cgratr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ kjh ”⟩ 𝒢 G ⟨“ xyz ”⟩
148 1 3 54 77 58 65 66 74 75 76 147 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ xyz ”⟩ 𝒢 G ⟨“ kjh ”⟩
149 1 3 54 77 55 68 69 74 75 76 80 58 65 66 148 cgratr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ wvt ”⟩ 𝒢 G ⟨“ kjh ”⟩
150 144 149 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ wvt ”⟩ ˙ ⟨“ kjh ”⟩
151 1 3 6 5 54 55 58 62 65 66 67 68 69 70 73 92 131 142 150 tgaaddcpbl2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ uvt ”⟩ ˙ ⟨“ ijh ”⟩
152 117 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z C = ⟨“ abc ”⟩
153 152 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a C = ⟨“ abc ”⟩
154 153 141 oveq12d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a C + ˙ D = ⟨“ abc ”⟩ + ˙ ⟨“ ijk ”⟩
155 simp-8r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z i j
156 155 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x i j
157 156 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a i j
158 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j a b
159 158 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z a b
160 159 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x a b
161 160 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a a b
162 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j b c
163 162 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z b c
164 163 ad10antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x b c
165 164 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a b c
166 163 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z b c
167 159 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z a b
168 167 neneqd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z ¬ a = b
169 122 168 olcnd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z c a L b
170 1 3 6 22 109 110 108 166 169 167 lnrot1 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z a b L c
171 170 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x a b L c
172 171 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a a b L c
173 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a j - ˙ h = b - ˙ a
174 1 2 3 4 5 6 54 62 65 58 96 100 104 157 73 161 165 8 172 66 105 173 angmndaddov2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ abc ”⟩ + ˙ ⟨“ ijk ”⟩ = ⟨“ ijh ”⟩
175 154 174 eqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a C + ˙ D = ⟨“ ijh ”⟩
176 151 175 breqtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ uvt ”⟩ ˙ C + ˙ D
177 176 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a ⟨“ uvt ”⟩ ˙ C + ˙ D
178 1 2 3 4 5 6 23 61 64 57 95 99 103 156 72 160 164 171 angmndaddov2lem φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x ∃! h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a
179 reurex ∃! h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a
180 178 179 syl φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x h P ⟨“ kjh ”⟩ ˙ ⟨“ abc ”⟩ j - ˙ h = b - ˙ a
181 177 180 r19.29a φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x ⟨“ uvt ”⟩ ˙ C + ˙ D
182 53 181 eqbrtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x E + ˙ F ˙ C + ˙ D
183 182 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x E + ˙ F ˙ C + ˙ D
184 1 2 3 4 5 6 22 24 26 28 31 35 37 39 41 43 45 47 angmndaddov2lem φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z ∃! t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x
185 reurex ∃! t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x
186 184 185 syl φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z t P ⟨“ wvt ”⟩ ˙ ⟨“ xyz ”⟩ v - ˙ t = y - ˙ x
187 183 186 r19.29a φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z E + ˙ F ˙ C + ˙ D
188 15 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E = ⟨“ xyz ”⟩
189 simp-8r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x F = ⟨“ uvw ”⟩
190 188 189 oveq12d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E + ˙ F = ⟨“ xyz ”⟩ + ˙ ⟨“ uvw ”⟩
191 21 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v G 𝒢 Tarski
192 191 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x G 𝒢 Tarski
193 simp-11r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x u P
194 simp-10r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x v P
195 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x w P
196 30 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v x P
197 196 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x x P
198 33 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v y P
199 198 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y P
200 simp-4r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z z P
201 200 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v z P
202 201 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x z P
203 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x u v
204 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x v w
205 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z x y
206 205 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v x y
207 206 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x x y
208 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v y z
209 208 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y z
210 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ¬ x y L z
211 simp-4r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x t P
212 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩
213 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y - ˙ t = v - ˙ u
214 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y L z t I x
215 1 2 3 4 5 6 192 193 194 195 197 199 202 203 204 207 209 8 210 211 212 213 214 angmndaddov1 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ⟨“ xyz ”⟩ + ˙ ⟨“ uvw ”⟩ = ⟨“ xyt ”⟩
216 190 215 eqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E + ˙ F = ⟨“ xyt ”⟩
217 192 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a G 𝒢 Tarski
218 202 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a z P
219 102 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v c P
220 219 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x c P
221 220 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a c P
222 94 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v a P
223 222 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x a P
224 223 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a a P
225 98 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v b P
226 225 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x b P
227 226 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b P
228 simp-4r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a h P
229 197 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a x P
230 199 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a y P
231 211 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a t P
232 209 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a y z
233 163 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v b c
234 233 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x b c
235 234 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b c
236 21 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P G 𝒢 Tarski
237 236 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x G 𝒢 Tarski
238 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x t P
239 236 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z G 𝒢 Tarski
240 33 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P y P
241 240 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z y P
242 200 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P z P
243 242 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z z P
244 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P y z
245 244 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z y z
246 1 3 6 239 241 243 245 tgelrnln φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z y L z ran L
247 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l y L z
248 1 6 3 239 246 247 tglnpt φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l P
249 248 adantr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x l P
250 30 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P x P
251 250 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x x P
252 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x l t I x
253 1 4 3 237 238 249 251 252 tgbtwncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x l x I t
254 236 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t G 𝒢 Tarski
255 250 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t x P
256 248 adantr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t l P
257 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t t P
258 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t l x I t
259 1 4 3 254 255 256 257 258 tgbtwncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l x I t l t I x
260 253 259 impbida φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x l x I t
261 260 pm5.32da φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z l t I x l y L z l x I t
262 elin l y L z t I x l y L z l t I x
263 elin l y L z x I t l y L z l x I t
264 262 263 bibi12i l y L z t I x l y L z x I t l y L z l t I x l y L z l x I t
265 261 264 sylibr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u l y L z t I x l y L z x I t
266 265 eqrdv φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x = y L z x I t
267 266 neeq1d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y L z x I t
268 267 biimpa φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x y L z x I t
269 268 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a y L z x I t
270 192 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a G 𝒢 Tarski
271 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a h P
272 192 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c G 𝒢 Tarski
273 226 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c b P
274 220 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c c P
275 234 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c b c
276 1 3 6 272 273 274 275 tgelrnln φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c b L c ran L
277 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l b L c
278 1 6 3 272 276 277 tglnpt φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l P
279 278 adantr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a l P
280 223 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a a P
281 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a l h I a
282 1 4 3 270 271 279 280 281 tgbtwncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a l a I h
283 192 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h G 𝒢 Tarski
284 223 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h a P
285 278 adantr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h l P
286 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h h P
287 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h l a I h
288 1 4 3 283 284 285 286 287 tgbtwncom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l a I h l h I a
289 282 288 impbida φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a l a I h
290 289 pm5.32da φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c l h I a l b L c l a I h
291 elin l b L c h I a l b L c l h I a
292 elin l b L c a I h l b L c l a I h
293 291 292 bibi12i l b L c h I a l b L c a I h l b L c l h I a l b L c l a I h
294 290 293 sylibr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i l b L c h I a l b L c a I h
295 294 eqrdv φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a = b L c a I h
296 295 neeq1d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b L c a I h
297 296 biimpa φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b L c a I h
298 188 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a E = ⟨“ xyz ”⟩
299 115 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v E ˙ C
300 299 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E ˙ C
301 300 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a E ˙ C
302 298 301 eqbrtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ xyz ”⟩ ˙ C
303 117 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z C = ⟨“ abc ”⟩
304 303 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a C = ⟨“ abc ”⟩
305 302 304 breqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ xyz ”⟩ ˙ ⟨“ abc ”⟩
306 143 a1i φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a 𝒢 G = ˙
307 193 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a u P
308 194 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a v P
309 195 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a w P
310 5 a1i φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ˙ = 𝒢 G
311 212 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩
312 310 311 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ zyt ”⟩ 𝒢 G ⟨“ uvw ”⟩
313 60 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v i P
314 313 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x i P
315 314 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a i P
316 63 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v j P
317 316 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x j P
318 317 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a j P
319 56 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v k P
320 319 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x k P
321 320 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a k P
322 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩
323 310 322 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ cbh ”⟩ 𝒢 G ⟨“ ijk ”⟩
324 189 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a F = ⟨“ uvw ”⟩
325 135 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v F ˙ D
326 325 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x F ˙ D
327 326 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a F ˙ D
328 324 327 eqbrtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ uvw ”⟩ ˙ D
329 139 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z D = ⟨“ ijk ”⟩
330 329 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a D = ⟨“ ijk ”⟩
331 328 330 breqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ uvw ”⟩ ˙ ⟨“ ijk ”⟩
332 310 331 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ uvw ”⟩ 𝒢 G ⟨“ ijk ”⟩
333 1 3 217 77 307 308 309 315 318 321 332 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ ijk ”⟩ 𝒢 G ⟨“ uvw ”⟩
334 1 3 217 77 221 227 228 315 318 321 323 307 308 309 333 cgratr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ cbh ”⟩ 𝒢 G ⟨“ uvw ”⟩
335 1 3 217 77 221 227 228 307 308 309 334 cgracom φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ uvw ”⟩ 𝒢 G ⟨“ cbh ”⟩
336 1 3 217 77 218 230 231 307 308 309 312 221 227 228 335 cgratr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ zyt ”⟩ 𝒢 G ⟨“ cbh ”⟩
337 306 336 breqdi φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ zyt ”⟩ ˙ ⟨“ cbh ”⟩
338 1 3 6 5 217 218 221 224 227 228 229 230 231 232 235 269 297 305 337 tgaaddcpbl2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ xyt ”⟩ ˙ ⟨“ abh ”⟩
339 304 330 oveq12d φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a C + ˙ D = ⟨“ abc ”⟩ + ˙ ⟨“ ijk ”⟩
340 155 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v i j
341 340 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x i j
342 341 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a i j
343 71 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v j k
344 343 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x j k
345 344 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a j k
346 159 ad5antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v a b
347 346 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x a b
348 347 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a a b
349 94 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P a P
350 98 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P b P
351 102 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P c P
352 120 ad8antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ xyz ”⟩ 𝒢 G ⟨“ abc ”⟩
353 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ x y L z
354 244 neneqd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ y = z
355 ioran ¬ x y L z y = z ¬ x y L z ¬ y = z
356 353 354 355 sylanbrc φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ x y L z y = z
357 1 6 3 236 240 242 250 356 ncolrot2 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ z x L y x = y
358 1 3 4 236 250 240 242 349 350 351 352 6 357 cgrancol φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ c a L b a = b
359 1 6 3 236 349 350 351 358 ncolrot1 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ a b L c b = c
360 359 orsild φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ¬ a b L c
361 360 ad3antrrr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ¬ a b L c
362 361 ad4antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ¬ a b L c
363 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b - ˙ h = j - ˙ i
364 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a b L c h I a
365 1 2 3 4 5 6 217 315 318 321 224 227 221 342 345 348 235 8 362 228 322 363 364 angmndaddov1 φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ abc ”⟩ + ˙ ⟨“ ijk ”⟩ = ⟨“ abh ”⟩
366 339 365 eqtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a C + ˙ D = ⟨“ abh ”⟩
367 338 366 breqtrrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ xyt ”⟩ ˙ C + ˙ D
368 367 3anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a ⟨“ xyt ”⟩ ˙ C + ˙ D
369 1 2 3 4 5 6 192 314 317 320 223 226 220 341 344 347 234 361 angmndaddov1lem φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ∃! h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a
370 reurex ∃! h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a
371 369 370 syl φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x h P ⟨“ cbh ”⟩ ˙ ⟨“ ijk ”⟩ b - ˙ h = j - ˙ i b L c h I a
372 368 371 r19.29a φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x ⟨“ xyt ”⟩ ˙ C + ˙ D
373 216 372 eqbrtrd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E + ˙ F ˙ C + ˙ D
374 373 3anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x E + ˙ F ˙ C + ˙ D
375 21 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z G 𝒢 Tarski
376 simp-7r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z u P
377 simp-6r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z v P
378 simp-5r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z w P
379 30 ad7antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z x P
380 34 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z y P
381 simp-11r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z z P
382 simpllr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z u v
383 simplr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z v w
384 simp-9r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z x y
385 simp-8r φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z y z
386 simpr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z ¬ x y L z
387 1 2 3 4 5 6 375 376 377 378 379 380 381 382 383 384 385 386 angmndaddov1lem φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z ∃! t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x
388 reurex ∃! t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x
389 387 388 syl φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z t P ⟨“ zyt ”⟩ ˙ ⟨“ uvw ”⟩ y - ˙ t = v - ˙ u y L z t I x
390 374 389 r19.29a φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w ¬ x y L z E + ˙ F ˙ C + ˙ D
391 exmidd φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w x y L z ¬ x y L z
392 187 390 391 mpjaodan φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w E + ˙ F ˙ C + ˙ D
393 392 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w E + ˙ F ˙ C + ˙ D
394 393 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w E + ˙ F ˙ C + ˙ D
395 394 r19.29an φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w E + ˙ F ˙ C + ˙ D
396 1 fvexi P V
397 396 2 12 elcgrabasi φ u P v P w P F = ⟨“ uvw ”⟩ u v v w
398 397 ad9antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P u P v P w P F = ⟨“ uvw ”⟩ u v v w
399 398 ad9antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z u P v P w P F = ⟨“ uvw ”⟩ u v v w
400 395 399 r19.29vva φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E + ˙ F ˙ C + ˙ D
401 400 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E + ˙ F ˙ C + ˙ D
402 401 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E + ˙ F ˙ C + ˙ D
403 402 r19.29an φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z E + ˙ F ˙ C + ˙ D
404 396 2 11 elcgrabasi φ x P y P z P E = ⟨“ xyz ”⟩ x y y z
405 404 ad3antrrr φ a P b P c P x P y P z P E = ⟨“ xyz ”⟩ x y y z
406 405 ad9antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k x P y P z P E = ⟨“ xyz ”⟩ x y y z
407 403 406 r19.29vva φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k E + ˙ F ˙ C + ˙ D
408 407 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k E + ˙ F ˙ C + ˙ D
409 408 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k E + ˙ F ˙ C + ˙ D
410 409 r19.29an φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k E + ˙ F ˙ C + ˙ D
411 396 2 10 elcgrabasi φ i P j P k P D = ⟨“ ijk ”⟩ i j j k
412 411 ad6antr φ a P b P c P C = ⟨“ abc ”⟩ a b b c i P j P k P D = ⟨“ ijk ”⟩ i j j k
413 410 412 r19.29vva φ a P b P c P C = ⟨“ abc ”⟩ a b b c E + ˙ F ˙ C + ˙ D
414 413 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c E + ˙ F ˙ C + ˙ D
415 414 anasss φ a P b P c P C = ⟨“ abc ”⟩ a b b c E + ˙ F ˙ C + ˙ D
416 415 r19.29an φ a P b P c P C = ⟨“ abc ”⟩ a b b c E + ˙ F ˙ C + ˙ D
417 396 2 9 elcgrabasi φ a P b P c P C = ⟨“ abc ”⟩ a b b c
418 416 417 r19.29vva φ E + ˙ F ˙ C + ˙ D