stlei

Description: Ordering law for states. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	$⊢ A \in C_{ℋ}$
	stle.2	$⊢ B \in C_{ℋ}$
Assertion	stlei	$⊢ S \in States \to (A \subseteq B \to S (A) \leq S (B))$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$⊢ A \in C_{ℋ}$
2		stle.2	$⊢ B \in C_{ℋ}$
3	2	chshii	$⊢ B \in S_{ℋ}$
4		shococss	$⊢ B \in S_{ℋ} \to B \subseteq ⊥ (⊥ (B))$
5	3 4	ax-mp	$⊢ B \subseteq ⊥ (⊥ (B))$
6		sstr2	$⊢ A \subseteq B \to (B \subseteq ⊥ (⊥ (B)) \to A \subseteq ⊥ (⊥ (B)))$
7	5 6	mpi	$⊢ A \subseteq B \to A \subseteq ⊥ (⊥ (B))$
8	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
9	1 8	pm3.2i	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ})$
10	7 9	jctil	$⊢ A \subseteq B \to ((A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \land A \subseteq ⊥ (⊥ (B)))$
11		stj	$⊢ S \in States \to (((A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \land A \subseteq ⊥ (⊥ (B))) \to S (A \lor_{ℋ} ⊥ (B)) = S (A) + S (⊥ (B)))$
12	10 11	syl5	$⊢ S \in States \to (A \subseteq B \to S (A \lor_{ℋ} ⊥ (B)) = S (A) + S (⊥ (B)))$
13	12	imp	$⊢ (S \in States \land A \subseteq B) \to S (A \lor_{ℋ} ⊥ (B)) = S (A) + S (⊥ (B))$
14	1 8	chjcli	$⊢ A \lor_{ℋ} ⊥ (B) \in C_{ℋ}$
15		stle1	$⊢ S \in States \to (A \lor_{ℋ} ⊥ (B) \in C_{ℋ} \to S (A \lor_{ℋ} ⊥ (B)) \leq 1)$
16	14 15	mpi	$⊢ S \in States \to S (A \lor_{ℋ} ⊥ (B)) \leq 1$
17	2	sto1i	$⊢ S \in States \to S (B) + S (⊥ (B)) = 1$
18	16 17	breqtrrd	$⊢ S \in States \to S (A \lor_{ℋ} ⊥ (B)) \leq S (B) + S (⊥ (B))$
19	18	adantr	$⊢ (S \in States \land A \subseteq B) \to S (A \lor_{ℋ} ⊥ (B)) \leq S (B) + S (⊥ (B))$
20	13 19	eqbrtrrd	$⊢ (S \in States \land A \subseteq B) \to S (A) + S (⊥ (B)) \leq S (B) + S (⊥ (B))$
21		stcl	$⊢ S \in States \to (A \in C_{ℋ} \to S (A) \in ℝ)$
22	1 21	mpi	$⊢ S \in States \to S (A) \in ℝ$
23		stcl	$⊢ S \in States \to (B \in C_{ℋ} \to S (B) \in ℝ)$
24	2 23	mpi	$⊢ S \in States \to S (B) \in ℝ$
25		stcl	$⊢ S \in States \to (⊥ (B) \in C_{ℋ} \to S (⊥ (B)) \in ℝ)$
26	8 25	mpi	$⊢ S \in States \to S (⊥ (B)) \in ℝ$
27	22 24 26	3jca	$⊢ S \in States \to (S (A) \in ℝ \land S (B) \in ℝ \land S (⊥ (B)) \in ℝ)$
28	27	adantr	$⊢ (S \in States \land A \subseteq B) \to (S (A) \in ℝ \land S (B) \in ℝ \land S (⊥ (B)) \in ℝ)$
29		leadd1	$⊢ (S (A) \in ℝ \land S (B) \in ℝ \land S (⊥ (B)) \in ℝ) \to (S (A) \leq S (B) \leftrightarrow S (A) + S (⊥ (B)) \leq S (B) + S (⊥ (B)))$
30	28 29	syl	$⊢ (S \in States \land A \subseteq B) \to (S (A) \leq S (B) \leftrightarrow S (A) + S (⊥ (B)) \leq S (B) + S (⊥ (B)))$
31	20 30	mpbird	$⊢ (S \in States \land A \subseteq B) \to S (A) \leq S (B)$
32	31	ex	$⊢ S \in States \to (A \subseteq B \to S (A) \leq S (B))$

Metamath Proof Explorer

Theorem stlei

Proof