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 e. CH
golem1.2 
|- B e. CH
golem1.3 
|- C e. CH
golem1.4 
|- F = ( ( _|_ ` A ) vH ( A i^i B ) )
golem1.5 
|- G = ( ( _|_ ` B ) vH ( B i^i C ) )
golem1.6 
|- H = ( ( _|_ ` C ) vH ( C i^i A ) )
golem1.7 
|- D = ( ( _|_ ` B ) vH ( B i^i A ) )
golem1.8 
|- R = ( ( _|_ ` C ) vH ( C i^i B ) )
golem1.9 
|- S = ( ( _|_ ` A ) vH ( A i^i C ) )
Assertion golem1 
|- ( f e. States -> ( ( ( f ` F ) + ( f ` G ) ) + ( f ` H ) ) = ( ( ( f ` D ) + ( f ` R ) ) + ( f ` S ) ) )

Proof

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