Metamath Proof Explorer

Theorem golem2

Description: Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999) (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 golem2 
|- ( f e. States -> ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( f ` D ) = 1 ) )

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 1 2 chincli 
 |-  ( A i^i B ) e. CH
12 10 11 chjcli 
 |-  ( ( _|_ ` A ) vH ( A i^i B ) ) e. CH
13 4 12 eqeltri 
 |-  F e. CH
14 2 choccli 
 |-  ( _|_ ` B ) e. CH
15 2 3 chincli 
 |-  ( B i^i C ) e. CH
16 14 15 chjcli 
 |-  ( ( _|_ ` B ) vH ( B i^i C ) ) e. CH
17 5 16 eqeltri 
 |-  G e. CH
18 3 choccli 
 |-  ( _|_ ` C ) e. CH
19 3 1 chincli 
 |-  ( C i^i A ) e. CH
20 18 19 chjcli 
 |-  ( ( _|_ ` C ) vH ( C i^i A ) ) e. CH
21 6 20 eqeltri 
 |-  H e. CH
22 13 17 21 stm1add3i 
 |-  ( f e. States -> ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( ( ( f ` F ) + ( f ` G ) ) + ( f ` H ) ) = 3 ) )
23 1 2 3 4 5 6 7 8 9 golem1 
 |-  ( f e. States -> ( ( ( f ` F ) + ( f ` G ) ) + ( f ` H ) ) = ( ( ( f ` D ) + ( f ` R ) ) + ( f ` S ) ) )
24 23 eqeq1d 
 |-  ( f e. States -> ( ( ( ( f ` F ) + ( f ` G ) ) + ( f ` H ) ) = 3 <-> ( ( ( f ` D ) + ( f ` R ) ) + ( f ` S ) ) = 3 ) )
25 22 24 sylibd 
 |-  ( f e. States -> ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( ( ( f ` D ) + ( f ` R ) ) + ( f ` S ) ) = 3 ) )
26 2 1 chincli 
 |-  ( B i^i A ) e. CH
27 14 26 chjcli 
 |-  ( ( _|_ ` B ) vH ( B i^i A ) ) e. CH
28 7 27 eqeltri 
 |-  D e. CH
29 3 2 chincli 
 |-  ( C i^i B ) e. CH
30 18 29 chjcli 
 |-  ( ( _|_ ` C ) vH ( C i^i B ) ) e. CH
31 8 30 eqeltri 
 |-  R e. CH
32 1 3 chincli 
 |-  ( A i^i C ) e. CH
33 10 32 chjcli 
 |-  ( ( _|_ ` A ) vH ( A i^i C ) ) e. CH
34 9 33 eqeltri 
 |-  S e. CH
35 28 31 34 stadd3i 
 |-  ( f e. States -> ( ( ( ( f ` D ) + ( f ` R ) ) + ( f ` S ) ) = 3 -> ( f ` D ) = 1 ) )
36 25 35 syld 
 |-  ( f e. States -> ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( f ` D ) = 1 ) )