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 ⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
stcltr1.2 ⊢ 𝐴 ∈ Cℋ
stcltrlem1.3 ⊢ 𝐵 ∈ Cℋ
Assertion stcltrlem1 ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) = 1 → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 stcltr1.1 ⊢ ( 𝜑 ↔ ( 𝑆 ∈ States ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( ( ( 𝑆 ‘ 𝑥 ) = 1 → ( 𝑆 ‘ 𝑦 ) = 1 ) → 𝑥 ⊆ 𝑦 ) ) )
2 stcltr1.2 ⊢ 𝐴 ∈ Cℋ
3 stcltrlem1.3 ⊢ 𝐵 ∈ Cℋ
4 1 simplbi ⊢ ( 𝜑 → 𝑆 ∈ States )
5 2 3 stji1i ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
6 4 5 syl ⊢ ( 𝜑 → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )
8 1 3 stcltr2i ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) = 1 → 𝐵 = ℋ ) )
9 8 imp ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝐵 = ℋ )
10 ineq2 ⊢ ( 𝐵 = ℋ → ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∩ ℋ ) )
11 2 chm1i ⊢ ( 𝐴 ∩ ℋ ) = 𝐴
12 10 11 eqtrdi ⊢ ( 𝐵 = ℋ → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
13 9 12 syl ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
14 13 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑆 ‘ 𝐴 ) )
15 14 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ 𝐴 ) ) )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → 𝑆 ∈ States )
17 2 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
18 stcl ⊢ ( 𝑆 ∈ States → ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ ) )
19 17 18 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℝ )
20 19 recnd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ∈ ℂ )
21 stcl ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
22 2 21 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
23 22 recnd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℂ )
24 20 23 addcomd ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ 𝐴 ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) )
25 2 sto1i ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) ) = 1 )
26 24 25 eqtrd ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ 𝐴 ) ) = 1 )
27 16 26 syl ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ 𝐴 ) ) = 1 )
28 15 27 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( ( 𝑆 ‘ ( ⊥ ‘ 𝐴 ) ) + ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) ) = 1 )
29 7 28 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝐵 ) = 1 ) → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = 1 )
30 29 ex ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) = 1 → ( 𝑆 ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) = 1 ) )