Metamath Proof Explorer

Theorem stcltrlem1

Description: Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stcltr1.1 
|- ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
stcltr1.2 
|- A e. CH
stcltrlem1.3 
|- B e. CH
Assertion stcltrlem1 
|- ( ph -> ( ( S ` B ) = 1 -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 stcltr1.1 
 |-  ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
2 stcltr1.2 
 |-  A e. CH
3 stcltrlem1.3 
 |-  B e. CH
4 1 simplbi 
 |-  ( ph -> S e. States )
5 2 3 stji1i 
 |-  ( S e. States -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) )
6 4 5 syl 
 |-  ( ph -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) )
7 6 adantr 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) )
8 1 3 stcltr2i 
 |-  ( ph -> ( ( S ` B ) = 1 -> B = ~H ) )
9 8 imp 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> B = ~H )
10 ineq2 
 |-  ( B = ~H -> ( A i^i B ) = ( A i^i ~H ) )
11 2 chm1i 
 |-  ( A i^i ~H ) = A
12 10 11 eqtrdi 
 |-  ( B = ~H -> ( A i^i B ) = A )
13 9 12 syl 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( A i^i B ) = A )
14 13 fveq2d 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( S ` ( A i^i B ) ) = ( S ` A ) )
15 14 oveq2d 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` A ) ) )
16 4 adantr 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> S e. States )
17 2 choccli 
 |-  ( _|_ ` A ) e. CH
18 stcl 
 |-  ( S e. States -> ( ( _|_ ` A ) e. CH -> ( S ` ( _|_ ` A ) ) e. RR ) )
19 17 18 mpi 
 |-  ( S e. States -> ( S ` ( _|_ ` A ) ) e. RR )
20 19 recnd 
 |-  ( S e. States -> ( S ` ( _|_ ` A ) ) e. CC )
21 stcl 
 |-  ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) )
22 2 21 mpi 
 |-  ( S e. States -> ( S ` A ) e. RR )
23 22 recnd 
 |-  ( S e. States -> ( S ` A ) e. CC )
24 20 23 addcomd 
 |-  ( S e. States -> ( ( S ` ( _|_ ` A ) ) + ( S ` A ) ) = ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) )
25 2 sto1i 
 |-  ( S e. States -> ( ( S ` A ) + ( S ` ( _|_ ` A ) ) ) = 1 )
26 24 25 eqtrd 
 |-  ( S e. States -> ( ( S ` ( _|_ ` A ) ) + ( S ` A ) ) = 1 )
27 16 26 syl 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( ( S ` ( _|_ ` A ) ) + ( S ` A ) ) = 1 )
28 15 27 eqtrd 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) = 1 )
29 7 28 eqtrd 
 |-  ( ( ph /\ ( S ` B ) = 1 ) -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = 1 )
30 29 ex 
 |-  ( ph -> ( ( S ` B ) = 1 -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = 1 ) )