thlleval

Description: Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015)

	Ref	Expression
Hypotheses	thlval.k	$⊢ K = toHL (W)$
	thlbas.c	$⊢ C = ClSubSp (W)$
	thlleval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
Assertion	thlleval	$⊢ (S \in C \land T \in C) \to (S \underset{˙}{\leq} T \leftrightarrow S \subseteq T)$

Step	Hyp	Ref	Expression
1		thlval.k	$⊢ K = toHL (W)$
2		thlbas.c	$⊢ C = ClSubSp (W)$
3		thlleval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4	2	fvexi	$⊢ C \in V$
5		eqid	$⊢ toInc (C) = toInc (C)$
6		eqid	$⊢ \leq_{toInc (C)} = \leq_{toInc (C)}$
7	1 2 5 6	thlle	$⊢ \leq_{toInc (C)} = \leq_{K}$
8	3 7	eqtr4i	$⊢ \underset{˙}{\leq} = \leq_{toInc (C)}$
9	5 8	ipole	$⊢ (C \in V \land S \in C \land T \in C) \to (S \underset{˙}{\leq} T \leftrightarrow S \subseteq T)$
10	4 9	mp3an1	$⊢ (S \in C \land T \in C) \to (S \underset{˙}{\leq} T \leftrightarrow S \subseteq T)$

Metamath Proof Explorer