stcltrlem1

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

	Ref	Expression
Hypotheses	stcltr1.1	$⊢ φ \leftrightarrow (S \in States \land \forall x \in C_{ℋ} \forall y \in C_{ℋ} ((S (x) = 1 \to S (y) = 1) \to x \subseteq y))$
	stcltr1.2	$⊢ A \in C_{ℋ}$
	stcltrlem1.3	$⊢ B \in C_{ℋ}$
Assertion	stcltrlem1	$⊢ φ \to (S (B) = 1 \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = 1)$

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	$⊢ φ \leftrightarrow (S \in States \land \forall x \in C_{ℋ} \forall y \in C_{ℋ} ((S (x) = 1 \to S (y) = 1) \to x \subseteq y))$
2		stcltr1.2	$⊢ A \in C_{ℋ}$
3		stcltrlem1.3	$⊢ B \in C_{ℋ}$
4	1	simplbi	$⊢ φ \to S \in States$
5	2 3	stji1i	$⊢ S \in States \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = S (⊥ (A)) + S (A \cap B)$
6	4 5	syl	$⊢ φ \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = S (⊥ (A)) + S (A \cap B)$
7	6	adantr	$⊢ (φ \land S (B) = 1) \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = S (⊥ (A)) + S (A \cap B)$
8	1 3	stcltr2i	$⊢ φ \to (S (B) = 1 \to B = ℋ)$
9	8	imp	$⊢ (φ \land S (B) = 1) \to B = ℋ$
10		ineq2	$⊢ B = ℋ \to A \cap B = A \cap ℋ$
11	2	chm1i	$⊢ A \cap ℋ = A$
12	10 11	eqtrdi	$⊢ B = ℋ \to A \cap B = A$
13	9 12	syl	$⊢ (φ \land S (B) = 1) \to A \cap B = A$
14	13	fveq2d	$⊢ (φ \land S (B) = 1) \to S (A \cap B) = S (A)$
15	14	oveq2d	$⊢ (φ \land S (B) = 1) \to S (⊥ (A)) + S (A \cap B) = S (⊥ (A)) + S (A)$
16	4	adantr	$⊢ (φ \land S (B) = 1) \to S \in States$
17	2	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
18		stcl	$⊢ S \in States \to (⊥ (A) \in C_{ℋ} \to S (⊥ (A)) \in ℝ)$
19	17 18	mpi	$⊢ S \in States \to S (⊥ (A)) \in ℝ$
20	19	recnd	$⊢ S \in States \to S (⊥ (A)) \in ℂ$
21		stcl	$⊢ S \in States \to (A \in C_{ℋ} \to S (A) \in ℝ)$
22	2 21	mpi	$⊢ S \in States \to S (A) \in ℝ$
23	22	recnd	$⊢ S \in States \to S (A) \in ℂ$
24	20 23	addcomd	$⊢ S \in States \to S (⊥ (A)) + S (A) = S (A) + S (⊥ (A))$
25	2	sto1i	$⊢ S \in States \to S (A) + S (⊥ (A)) = 1$
26	24 25	eqtrd	$⊢ S \in States \to S (⊥ (A)) + S (A) = 1$
27	16 26	syl	$⊢ (φ \land S (B) = 1) \to S (⊥ (A)) + S (A) = 1$
28	15 27	eqtrd	$⊢ (φ \land S (B) = 1) \to S (⊥ (A)) + S (A \cap B) = 1$
29	7 28	eqtrd	$⊢ (φ \land S (B) = 1) \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = 1$
30	29	ex	$⊢ φ \to (S (B) = 1 \to S (⊥ (A) \lor_{ℋ} (A \cap B)) = 1)$

Metamath Proof Explorer

Theorem stcltrlem1

Proof