dihglblem5

Description: Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014)

	Ref	Expression
Hypotheses	dihglblem5.b	$⊢ B = {Base}_{K}$
	dihglblem5.g	$⊢ G = glb (K)$
	dihglblem5.h	$⊢ H = LHyp (K)$
	dihglblem5.u	$⊢ U = DVecH (K) (W)$
	dihglblem5.i	$⊢ I = DIsoH (K) (W)$
	dihglblem5.s	$⊢ S = LSubSp (U)$
Assertion	dihglblem5	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to ⋂_{x \in T} I (x) \in S$

Proof

Step	Hyp	Ref	Expression
1		dihglblem5.b	$⊢ B = {Base}_{K}$
2		dihglblem5.g	$⊢ G = glb (K)$
3		dihglblem5.h	$⊢ H = LHyp (K)$
4		dihglblem5.u	$⊢ U = DVecH (K) (W)$
5		dihglblem5.i	$⊢ I = DIsoH (K) (W)$
6		dihglblem5.s	$⊢ S = LSubSp (U)$
7		fvex	$⊢ I (x) \in V$
8	7	dfiin2	$⊢ ⋂_{x \in T} I (x) = ⋂ \{y \| \exists x \in T y = I (x)\}$
9		simpl	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to (K \in HL \land W \in H)$
10	3 4 9	dvhlmod	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to U \in LMod$
11		simpll	$⊢ (((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \land x \in T) \to (K \in HL \land W \in H)$
12		simplrl	$⊢ (((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \land x \in T) \to T \subseteq B$
13		simpr	$⊢ (((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \land x \in T) \to x \in T$
14	12 13	sseldd	$⊢ (((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \land x \in T) \to x \in B$
15	1 3 5 4 6	dihlss	$⊢ ((K \in HL \land W \in H) \land x \in B) \to I (x) \in S$
16	11 14 15	syl2anc	$⊢ (((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \land x \in T) \to I (x) \in S$
17	16	ralrimiva	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to \forall x \in T I (x) \in S$
18		uniiunlem	$⊢ \forall x \in T I (x) \in S \to (\forall x \in T I (x) \in S \leftrightarrow \{y \| \exists x \in T y = I (x)\} \subseteq S)$
19	17 18	syl	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to (\forall x \in T I (x) \in S \leftrightarrow \{y \| \exists x \in T y = I (x)\} \subseteq S)$
20	17 19	mpbid	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to \{y \| \exists x \in T y = I (x)\} \subseteq S$
21		simprr	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to T \neq \emptyset$
22		n0	$⊢ T \neq \emptyset \leftrightarrow \exists x x \in T$
23	21 22	sylib	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to \exists x x \in T$
24		nfre1	$⊢ Ⅎ x \exists x \in T y = I (x)$
25	24	nfab	$⊢ \underline{Ⅎ} x \{y \| \exists x \in T y = I (x)\}$
26		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
27	25 26	nfne	$⊢ Ⅎ x \{y \| \exists x \in T y = I (x)\} \neq \emptyset$
28	7	elabrex	$⊢ x \in T \to I (x) \in \{y \| \exists x \in T y = I (x)\}$
29	28	ne0d	$⊢ x \in T \to \{y \| \exists x \in T y = I (x)\} \neq \emptyset$
30	27 29	exlimi	$⊢ \exists x x \in T \to \{y \| \exists x \in T y = I (x)\} \neq \emptyset$
31	23 30	syl	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to \{y \| \exists x \in T y = I (x)\} \neq \emptyset$
32	6	lssintcl	$⊢ (U \in LMod \land \{y \| \exists x \in T y = I (x)\} \subseteq S \land \{y \| \exists x \in T y = I (x)\} \neq \emptyset) \to ⋂ \{y \| \exists x \in T y = I (x)\} \in S$
33	10 20 31 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to ⋂ \{y \| \exists x \in T y = I (x)\} \in S$
34	8 33	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (T \subseteq B \land T \neq \emptyset)) \to ⋂_{x \in T} I (x) \in S$

Metamath Proof Explorer

Theorem dihglblem5

Proof