Metamath Proof Explorer

Theorem goeqi

Description: Godowski's equation, shown here as a variant equivalent to Equation SF of Godowski p. 730. (Contributed by NM, 10-Nov-2002) (New usage is discouraged.)

Ref Expression
Hypotheses goeq.1 
|- A e. CH
goeq.2 
|- B e. CH
goeq.3 
|- C e. CH
goeq.4 
|- F = ( ( _|_ ` A ) vH ( A i^i B ) )
goeq.5 
|- G = ( ( _|_ ` B ) vH ( B i^i C ) )
goeq.6 
|- H = ( ( _|_ ` C ) vH ( C i^i A ) )
goeq.7 
|- D = ( ( _|_ ` B ) vH ( B i^i A ) )
Assertion goeqi 
|- ( ( F i^i G ) i^i H ) C_ D

Proof

Step Hyp Ref Expression
1 goeq.1 
 |-  A e. CH
2 goeq.2 
 |-  B e. CH
3 goeq.3 
 |-  C e. CH
4 goeq.4 
 |-  F = ( ( _|_ ` A ) vH ( A i^i B ) )
5 goeq.5 
 |-  G = ( ( _|_ ` B ) vH ( B i^i C ) )
6 goeq.6 
 |-  H = ( ( _|_ ` C ) vH ( C i^i A ) )
7 goeq.7 
 |-  D = ( ( _|_ ` B ) vH ( B i^i A ) )
8 1 choccli 
 |-  ( _|_ ` A ) e. CH
9 1 2 chincli 
 |-  ( A i^i B ) e. CH
10 8 9 chjcli 
 |-  ( ( _|_ ` A ) vH ( A i^i B ) ) e. CH
11 4 10 eqeltri 
 |-  F e. CH
12 2 choccli 
 |-  ( _|_ ` B ) e. CH
13 2 3 chincli 
 |-  ( B i^i C ) e. CH
14 12 13 chjcli 
 |-  ( ( _|_ ` B ) vH ( B i^i C ) ) e. CH
15 5 14 eqeltri 
 |-  G e. CH
16 11 15 chincli 
 |-  ( F i^i G ) e. CH
17 3 choccli 
 |-  ( _|_ ` C ) e. CH
18 3 1 chincli 
 |-  ( C i^i A ) e. CH
19 17 18 chjcli 
 |-  ( ( _|_ ` C ) vH ( C i^i A ) ) e. CH
20 6 19 eqeltri 
 |-  H e. CH
21 16 20 chincli 
 |-  ( ( F i^i G ) i^i H ) e. CH
22 2 1 chincli 
 |-  ( B i^i A ) e. CH
23 12 22 chjcli 
 |-  ( ( _|_ ` B ) vH ( B i^i A ) ) e. CH
24 7 23 eqeltri 
 |-  D e. CH
25 21 24 stri 
 |-  ( A. f e. States ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( f ` D ) = 1 ) -> ( ( F i^i G ) i^i H ) C_ D )
26 eqid 
 |-  ( ( _|_ ` C ) vH ( C i^i B ) ) = ( ( _|_ ` C ) vH ( C i^i B ) )
27 eqid 
 |-  ( ( _|_ ` A ) vH ( A i^i C ) ) = ( ( _|_ ` A ) vH ( A i^i C ) )
28 1 2 3 4 5 6 7 26 27 golem2 
 |-  ( f e. States -> ( ( f ` ( ( F i^i G ) i^i H ) ) = 1 -> ( f ` D ) = 1 ) )
29 25 28 mprg 
 |-  ( ( F i^i G ) i^i H ) C_ D