Metamath Proof Explorer


Theorem golem1

Description: Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002) (New usage is discouraged.)

Ref Expression
Hypotheses golem1.1 A C
golem1.2 B C
golem1.3 C C
golem1.4 F = A A B
golem1.5 G = B B C
golem1.6 H = C C A
golem1.7 D = B B A
golem1.8 R = C C B
golem1.9 S = A A C
Assertion golem1 f States f F + f G + f H = f D + f R + f S

Proof

Step Hyp Ref Expression
1 golem1.1 A C
2 golem1.2 B C
3 golem1.3 C C
4 golem1.4 F = A A B
5 golem1.5 G = B B C
6 golem1.6 H = C C A
7 golem1.7 D = B B A
8 golem1.8 R = C C B
9 golem1.9 S = A A C
10 1 choccli A C
11 stcl f States A C f A
12 10 11 mpi f States f A
13 12 recnd f States f A
14 2 choccli B C
15 stcl f States B C f B
16 14 15 mpi f States f B
17 16 recnd f States f B
18 3 choccli C C
19 stcl f States C C f C
20 18 19 mpi f States f C
21 20 recnd f States f C
22 13 17 21 addassd f States f A + f B + f C = f A + f B + f C
23 17 21 addcld f States f B + f C
24 13 23 addcomd f States f A + f B + f C = f B + f C + f A
25 22 24 eqtrd f States f A + f B + f C = f B + f C + f A
26 25 oveq1d f States f A + f B + f C + f A B + f B C + f C A = f B + f C + f A + f A B + f B C + f C A
27 13 17 addcld f States f A + f B
28 1 2 chincli A B C
29 stcl f States A B C f A B
30 28 29 mpi f States f A B
31 30 recnd f States f A B
32 2 3 chincli B C C
33 stcl f States B C C f B C
34 32 33 mpi f States f B C
35 34 recnd f States f B C
36 31 35 addcld f States f A B + f B C
37 3 1 chincli C A C
38 stcl f States C A C f C A
39 37 38 mpi f States f C A
40 39 recnd f States f C A
41 27 36 21 40 add4d f States f A + f B + f A B + f B C + f C + f C A = f A + f B + f C + f A B + f B C + f C A
42 23 36 13 40 add4d f States f B + f C + f A B + f B C + f A + f C A = f B + f C + f A + f A B + f B C + f C A
43 26 41 42 3eqtr4d f States f A + f B + f A B + f B C + f C + f C A = f B + f C + f A B + f B C + f A + f C A
44 13 31 17 35 add4d f States f A + f A B + f B + f B C = f A + f B + f A B + f B C
45 44 oveq1d f States f A + f A B + f B + f B C + f C + f C A = f A + f B + f A B + f B C + f C + f C A
46 17 31 21 35 add4d f States f B + f A B + f C + f B C = f B + f C + f A B + f B C
47 46 oveq1d f States f B + f A B + f C + f B C + f A + f C A = f B + f C + f A B + f B C + f A + f C A
48 43 45 47 3eqtr4d f States f A + f A B + f B + f B C + f C + f C A = f B + f A B + f C + f B C + f A + f C A
49 1 2 stji1i f States f A A B = f A + f A B
50 2 3 stji1i f States f B B C = f B + f B C
51 49 50 oveq12d f States f A A B + f B B C = f A + f A B + f B + f B C
52 3 1 stji1i f States f C C A = f C + f C A
53 51 52 oveq12d f States f A A B + f B B C + f C C A = f A + f A B + f B + f B C + f C + f C A
54 2 1 stji1i f States f B B A = f B + f B A
55 incom B A = A B
56 55 fveq2i f B A = f A B
57 56 oveq2i f B + f B A = f B + f A B
58 54 57 eqtrdi f States f B B A = f B + f A B
59 3 2 stji1i f States f C C B = f C + f C B
60 incom C B = B C
61 60 fveq2i f C B = f B C
62 61 oveq2i f C + f C B = f C + f B C
63 59 62 eqtrdi f States f C C B = f C + f B C
64 58 63 oveq12d f States f B B A + f C C B = f B + f A B + f C + f B C
65 1 3 stji1i f States f A A C = f A + f A C
66 incom A C = C A
67 66 fveq2i f A C = f C A
68 67 oveq2i f A + f A C = f A + f C A
69 65 68 eqtrdi f States f A A C = f A + f C A
70 64 69 oveq12d f States f B B A + f C C B + f A A C = f B + f A B + f C + f B C + f A + f C A
71 48 53 70 3eqtr4d f States f A A B + f B B C + f C C A = f B B A + f C C B + f A A C
72 4 fveq2i f F = f A A B
73 5 fveq2i f G = f B B C
74 72 73 oveq12i f F + f G = f A A B + f B B C
75 6 fveq2i f H = f C C A
76 74 75 oveq12i f F + f G + f H = f A A B + f B B C + f C C A
77 7 fveq2i f D = f B B A
78 8 fveq2i f R = f C C B
79 77 78 oveq12i f D + f R = f B B A + f C C B
80 9 fveq2i f S = f A A C
81 79 80 oveq12i f D + f R + f S = f B B A + f C C B + f A A C
82 71 76 81 3eqtr4g f States f F + f G + f H = f D + f R + f S