dihintcl

Description: The intersection of closed subspaces (the range of isomorphism H) is a closed subspace. (Contributed by NM, 14-Apr-2014)

	Ref	Expression
Hypotheses	dihintcl.h	$⊢ H = LHyp (K)$
	dihintcl.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihintcl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂ S \in ran I$

Proof

Step	Hyp	Ref	Expression
1		dihintcl.h	$⊢ H = LHyp (K)$
2		dihintcl.i	$⊢ I = DIsoH (K) (W)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4	3 1 2	dihfn	$⊢ (K \in HL \land W \in H) \to I Fn {Base}_{K}$
5	3 1 2	dihdm	$⊢ (K \in HL \land W \in H) \to dom I = {Base}_{K}$
6	5	fneq2d	$⊢ (K \in HL \land W \in H) \to (I Fn dom I \leftrightarrow I Fn {Base}_{K})$
7	4 6	mpbird	$⊢ (K \in HL \land W \in H) \to I Fn dom I$
8	7	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I Fn dom I$
9		cnvimass	$⊢ I^{-1} [S] \subseteq dom I$
10		fnssres	$⊢ (I Fn dom I \land I^{-1} [S] \subseteq dom I) \to ({I ↾}_{I^{-1} [S]}) Fn I^{-1} [S]$
11	8 9 10	sylancl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ({I ↾}_{I^{-1} [S]}) Fn I^{-1} [S]$
12		fniinfv	$⊢ ({I ↾}_{I^{-1} [S]}) Fn I^{-1} [S] \to ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) = ⋂ ran ({I ↾}_{I^{-1} [S]})$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) = ⋂ ran ({I ↾}_{I^{-1} [S]})$
14		df-ima	$⊢ I [I^{-1} [S]] = ran ({I ↾}_{I^{-1} [S]})$
15	4	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I Fn {Base}_{K}$
16		dffn4	$⊢ I Fn {Base}_{K} \leftrightarrow I : {Base}_{K} \underset{onto}{⟶} ran I$
17	15 16	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I : {Base}_{K} \underset{onto}{⟶} ran I$
18		simprl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to S \subseteq ran I$
19		foimacnv	$⊢ (I : {Base}_{K} \underset{onto}{⟶} ran I \land S \subseteq ran I) \to I [I^{-1} [S]] = S$
20	17 18 19	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I [I^{-1} [S]] = S$
21	14 20	eqtr3id	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ran ({I ↾}_{I^{-1} [S]}) = S$
22	21	inteqd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂ ran ({I ↾}_{I^{-1} [S]}) = ⋂ S$
23	13 22	eqtrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) = ⋂ S$
24		simpl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (K \in HL \land W \in H)$
25	5	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to dom I = {Base}_{K}$
26	9 25	sseqtrid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \subseteq {Base}_{K}$
27		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to S \neq \emptyset$
28		n0	$⊢ S \neq \emptyset \leftrightarrow \exists y y \in S$
29	27 28	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to \exists y y \in S$
30	18	sselda	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to y \in ran I$
31	25	fneq2d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (I Fn dom I \leftrightarrow I Fn {Base}_{K})$
32	15 31	mpbird	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I Fn dom I$
33	32	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to I Fn dom I$
34		fvelrnb	$⊢ I Fn dom I \to (y \in ran I \leftrightarrow \exists x \in dom I I (x) = y)$
35	33 34	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to (y \in ran I \leftrightarrow \exists x \in dom I I (x) = y)$
36	30 35	mpbid	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to \exists x \in dom I I (x) = y$
37		fnfun	$⊢ I Fn {Base}_{K} \to Fun I$
38	15 37	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to Fun I$
39		fvimacnv	$⊢ (Fun I \land x \in dom I) \to (I (x) \in S \leftrightarrow x \in I^{-1} [S])$
40	38 39	sylan	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land x \in dom I) \to (I (x) \in S \leftrightarrow x \in I^{-1} [S])$
41		ne0i	$⊢ x \in I^{-1} [S] \to I^{-1} [S] \neq \emptyset$
42	40 41	syl6bi	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land x \in dom I) \to (I (x) \in S \to I^{-1} [S] \neq \emptyset)$
43	42	ex	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (x \in dom I \to (I (x) \in S \to I^{-1} [S] \neq \emptyset))$
44		eleq1	$⊢ I (x) = y \to (I (x) \in S \leftrightarrow y \in S)$
45	44	biimprd	$⊢ I (x) = y \to (y \in S \to I (x) \in S)$
46	45	imim1d	$⊢ I (x) = y \to ((I (x) \in S \to I^{-1} [S] \neq \emptyset) \to (y \in S \to I^{-1} [S] \neq \emptyset))$
47	43 46	syl9	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (I (x) = y \to (x \in dom I \to (y \in S \to I^{-1} [S] \neq \emptyset)))$
48	47	com24	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (y \in S \to (x \in dom I \to (I (x) = y \to I^{-1} [S] \neq \emptyset)))$
49	48	imp	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to (x \in dom I \to (I (x) = y \to I^{-1} [S] \neq \emptyset))$
50	49	rexlimdv	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to (\exists x \in dom I I (x) = y \to I^{-1} [S] \neq \emptyset)$
51	36 50	mpd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to I^{-1} [S] \neq \emptyset$
52	29 51	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \neq \emptyset$
53		eqid	$⊢ glb (K) = glb (K)$
54	3 53 1 2	dihglb	$⊢ ((K \in HL \land W \in H) \land (I^{-1} [S] \subseteq {Base}_{K} \land I^{-1} [S] \neq \emptyset)) \to I (glb (K) (I^{-1} [S])) = ⋂_{y \in I^{-1} [S]} I (y)$
55	24 26 52 54	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I (glb (K) (I^{-1} [S])) = ⋂_{y \in I^{-1} [S]} I (y)$
56		fvres	$⊢ y \in I^{-1} [S] \to ({I ↾}_{I^{-1} [S]}) (y) = I (y)$
57	56	iineq2i	$⊢ ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) = ⋂_{y \in I^{-1} [S]} I (y)$
58	55 57	eqtr4di	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I (glb (K) (I^{-1} [S])) = ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y)$
59		hlclat	$⊢ K \in HL \to K \in CLat$
60	59	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to K \in CLat$
61	3 53	clatglbcl	$⊢ (K \in CLat \land I^{-1} [S] \subseteq {Base}_{K}) \to glb (K) (I^{-1} [S]) \in {Base}_{K}$
62	60 26 61	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to glb (K) (I^{-1} [S]) \in {Base}_{K}$
63	3 1 2	dihcl	$⊢ ((K \in HL \land W \in H) \land glb (K) (I^{-1} [S]) \in {Base}_{K}) \to I (glb (K) (I^{-1} [S])) \in ran I$
64	62 63	syldan	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I (glb (K) (I^{-1} [S])) \in ran I$
65	58 64	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) \in ran I$
66	23 65	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂ S \in ran I$

Metamath Proof Explorer

Theorem dihintcl

Proof