dibintclN

Description: The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibintcl.h	$⊢ H = LHyp (K)$
	dibintcl.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibintclN	$⊢ ((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		dibintcl.h	$⊢ H = LHyp (K)$
2		dibintcl.i	$⊢ I = DIsoB (K) (W)$
3	1 2	dibf11N	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{1-1 onto}{⟶} ran I$
4	3	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I : dom I \underset{1-1 onto}{⟶} ran I$
5		f1ofn	$⊢ I : dom I \underset{1-1 onto}{⟶} ran I \to I Fn dom I$
6	4 5	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I Fn dom I$
7		cnvimass	$⊢ I^{-1} [S] \subseteq dom I$
8		fnssres	$⊢ (I Fn dom I \land I^{-1} [S] \subseteq dom I) \to ({I ↾}_{I^{-1} [S]}) Fn I^{-1} [S]$
9	6 7 8	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]$
10		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]})$
11	9 10	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]})$
12		df-ima	$⊢ I [I^{-1} [S]] = ran ({I ↾}_{I^{-1} [S]})$
13		f1ofo	$⊢ I : dom I \underset{1-1 onto}{⟶} ran I \to I : dom I \underset{onto}{⟶} ran I$
14	3 13	syl	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{onto}{⟶} ran I$
15	14	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I : dom I \underset{onto}{⟶} ran I$
16		simprl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to S \subseteq ran I$
17		foimacnv	$⊢ (I : dom I \underset{onto}{⟶} ran I \land S \subseteq ran I) \to I [I^{-1} [S]] = S$
18	15 16 17	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I [I^{-1} [S]] = S$
19	12 18	eqtr3id	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ran ({I ↾}_{I^{-1} [S]}) = S$
20	19	inteqd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to ⋂ ran ({I ↾}_{I^{-1} [S]}) = ⋂ S$
21	11 20	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$
22		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)$
23	7	a1i	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \subseteq dom I$
24		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to S \neq \emptyset$
25		n0	$⊢ S \neq \emptyset \leftrightarrow \exists y y \in S$
26	24 25	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to \exists y y \in S$
27	16	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$
28	3	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in S) \to I : dom I \underset{1-1 onto}{⟶} ran I$
29	28 5	syl	$⊢ (((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$
30		fvelrnb	$⊢ I Fn dom I \to (y \in ran I \leftrightarrow \exists x \in dom I I (x) = y)$
31	29 30	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)$
32	27 31	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$
33		f1ofun	$⊢ I : dom I \underset{1-1 onto}{⟶} ran I \to Fun I$
34	3 33	syl	$⊢ (K \in HL \land W \in H) \to Fun I$
35	34	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to Fun I$
36		fvimacnv	$⊢ (Fun I \land x \in dom I) \to (I (x) \in S \leftrightarrow x \in I^{-1} [S])$
37	35 36	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])$
38		ne0i	$⊢ x \in I^{-1} [S] \to I^{-1} [S] \neq \emptyset$
39	37 38	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)$
40	39	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))$
41		eleq1	$⊢ I (x) = y \to (I (x) \in S \leftrightarrow y \in S)$
42	41	biimprd	$⊢ I (x) = y \to (y \in S \to I (x) \in S)$
43	42	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))$
44	40 43	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)))$
45	44	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)))$
46	45	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))$
47	46	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)$
48	32 47	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$
49	26 48	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \neq \emptyset$
50		eqid	$⊢ glb (K) = glb (K)$
51	50 1 2	dibglbN	$⊢ ((K \in HL \land W \in H) \land (I^{-1} [S] \subseteq dom I \land I^{-1} [S] \neq \emptyset)) \to I (glb (K) (I^{-1} [S])) = ⋂_{y \in I^{-1} [S]} I (y)$
52	22 23 49 51	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)$
53		fvres	$⊢ y \in I^{-1} [S] \to ({I ↾}_{I^{-1} [S]}) (y) = I (y)$
54	53	iineq2i	$⊢ ⋂_{y \in I^{-1} [S]} ({I ↾}_{I^{-1} [S]}) (y) = ⋂_{y \in I^{-1} [S]} I (y)$
55	52 54	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)$
56		hlclat	$⊢ K \in HL \to K \in CLat$
57	56	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to K \in CLat$
58		eqid	$⊢ {Base}_{K} = {Base}_{K}$
59		eqid	$⊢ \leq_{K} = \leq_{K}$
60	58 59 1 2	dibdmN	$⊢ (K \in HL \land W \in H) \to dom I = \{x \in {Base}_{K} \| x \leq_{K} W\}$
61		ssrab2	$⊢ \{x \in {Base}_{K} \| x \leq_{K} W\} \subseteq {Base}_{K}$
62	60 61	eqsstrdi	$⊢ (K \in HL \land W \in H) \to dom I \subseteq {Base}_{K}$
63	62	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to dom I \subseteq {Base}_{K}$
64	7 63	sstrid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \subseteq {Base}_{K}$
65	58 50	clatglbcl	$⊢ (K \in CLat \land I^{-1} [S] \subseteq {Base}_{K}) \to glb (K) (I^{-1} [S]) \in {Base}_{K}$
66	57 64 65	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}$
67		n0	$⊢ I^{-1} [S] \neq \emptyset \leftrightarrow \exists y y \in I^{-1} [S]$
68	49 67	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to \exists y y \in I^{-1} [S]$
69		hllat	$⊢ K \in HL \to K \in Lat$
70	69	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to K \in Lat$
71	66	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to glb (K) (I^{-1} [S]) \in {Base}_{K}$
72	64	sselda	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to y \in {Base}_{K}$
73	58 1	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
74	73	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to W \in {Base}_{K}$
75	56	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to K \in CLat$
76	60	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to dom I = \{x \in {Base}_{K} \| x \leq_{K} W\}$
77	7 76	sseqtrid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \subseteq \{x \in {Base}_{K} \| x \leq_{K} W\}$
78	77 61	sstrdi	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to I^{-1} [S] \subseteq {Base}_{K}$
79	78	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to I^{-1} [S] \subseteq {Base}_{K}$
80		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to y \in I^{-1} [S]$
81	58 59 50	clatglble	$⊢ (K \in CLat \land I^{-1} [S] \subseteq {Base}_{K} \land y \in I^{-1} [S]) \to glb (K) (I^{-1} [S]) \leq_{K} y$
82	75 79 80 81	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to glb (K) (I^{-1} [S]) \leq_{K} y$
83	7	sseli	$⊢ y \in I^{-1} [S] \to y \in dom I$
84	83	adantl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to y \in dom I$
85	58 59 1 2	dibeldmN	$⊢ (K \in HL \land W \in H) \to (y \in dom I \leftrightarrow (y \in {Base}_{K} \land y \leq_{K} W))$
86	85	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to (y \in dom I \leftrightarrow (y \in {Base}_{K} \land y \leq_{K} W))$
87	84 86	mpbid	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to (y \in {Base}_{K} \land y \leq_{K} W)$
88	87	simprd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to y \leq_{K} W$
89	58 59 70 71 72 74 82 88	lattrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \land y \in I^{-1} [S]) \to glb (K) (I^{-1} [S]) \leq_{K} W$
90	68 89	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to glb (K) (I^{-1} [S]) \leq_{K} W$
91	58 59 1 2	dibeldmN	$⊢ (K \in HL \land W \in H) \to (glb (K) (I^{-1} [S]) \in dom I \leftrightarrow (glb (K) (I^{-1} [S]) \in {Base}_{K} \land glb (K) (I^{-1} [S]) \leq_{K} W))$
92	91	adantr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to (glb (K) (I^{-1} [S]) \in dom I \leftrightarrow (glb (K) (I^{-1} [S]) \in {Base}_{K} \land glb (K) (I^{-1} [S]) \leq_{K} W))$
93	66 90 92	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (S \subseteq ran I \land S \neq \emptyset)) \to glb (K) (I^{-1} [S]) \in dom I$
94	1 2	dibclN	$⊢ ((K \in HL \land W \in H) \land glb (K) (I^{-1} [S]) \in dom I) \to I (glb (K) (I^{-1} [S])) \in ran I$
95	93 94	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$
96	55 95	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$
97	21 96	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 dibintclN

Proof