dihglblem6

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

	Ref	Expression
Hypotheses	dihglblem6.b	$⊢ B = {Base}_{K}$
	dihglblem6.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihglblem6.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglblem6.a	$⊢ A = Atoms (K)$
	dihglblem6.g	$⊢ G = glb (K)$
	dihglblem6.h	$⊢ H = LHyp (K)$
	dihglblem6.i	$⊢ I = DIsoH (K) (W)$
	dihglblem6.u	$⊢ U = DVecH (K) (W)$
	dihglblem6.s	$⊢ P = LSubSp (U)$
	dihglblem6.d	$⊢ D = LSAtoms (U)$
Assertion	dihglblem6	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Proof

Step	Hyp	Ref	Expression
1		dihglblem6.b	$⊢ B = {Base}_{K}$
2		dihglblem6.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihglblem6.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihglblem6.a	$⊢ A = Atoms (K)$
5		dihglblem6.g	$⊢ G = glb (K)$
6		dihglblem6.h	$⊢ H = LHyp (K)$
7		dihglblem6.i	$⊢ I = DIsoH (K) (W)$
8		dihglblem6.u	$⊢ U = DVecH (K) (W)$
9		dihglblem6.s	$⊢ P = LSubSp (U)$
10		dihglblem6.d	$⊢ D = LSAtoms (U)$
11		eqid	$⊢ meet (K) = meet (K)$
12		eqid	$⊢ \{u \in B \| \exists v \in S u = v meet (K) W\} = \{u \in B \| \exists v \in S u = v meet (K) W\}$
13		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
14	1 2 11 5 6 12 13 7	dihglblem4	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to I (G (S)) \subseteq ⋂_{x \in S} I (x)$
15		fal	$⊢ \neg ⊥$
16		simpll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to (K \in HL \land W \in H)$
17	6 8 16	dvhlmod	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to U \in LMod$
18		simplll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to K \in HL$
19		hlclat	$⊢ K \in HL \to K \in CLat$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to K \in CLat$
21		simplrl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to S \subseteq B$
22	1 5	clatglbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
23	20 21 22	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to G (S) \in B$
24	1 6 7 8 9	dihlss	$⊢ ((K \in HL \land W \in H) \land G (S) \in B) \to I (G (S)) \in P$
25	16 23 24	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to I (G (S)) \in P$
26	1 5 6 8 7 9	dihglblem5	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to ⋂_{x \in S} I (x) \in P$
27	26	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to ⋂_{x \in S} I (x) \in P$
28		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to I (G (S)) \subset ⋂_{x \in S} I (x)$
29	9 10 17 25 27 28	lpssat	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land I (G (S)) \subset ⋂_{x \in S} I (x)) \to \exists p \in D (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))$
30	29	ex	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to (I (G (S)) \subset ⋂_{x \in S} I (x) \to \exists p \in D (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S))))$
31		simp1l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to (K \in HL \land W \in H)$
32	6 8 7 10	dih1dimat	$⊢ ((K \in HL \land W \in H) \land p \in D) \to p \in ran I$
33	32	adantlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to p \in ran I$
34	33	3adant3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to p \in ran I$
35	6 7	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land p \in ran I) \to I (I^{-1} (p)) = p$
36	31 34 35	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to I (I^{-1} (p)) = p$
37		simp3l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to p \subseteq ⋂_{x \in S} I (x)$
38		ssiin	$⊢ p \subseteq ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S p \subseteq I (x)$
39	37 38	sylib	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to \forall x \in S p \subseteq I (x)$
40		simplll	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to (K \in HL \land W \in H)$
41		simpll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to (K \in HL \land W \in H)$
42	1 6 7 8 9	dihf11	$⊢ (K \in HL \land W \in H) \to I : B \underset{1-1}{⟶} P$
43		f1f1orn	$⊢ I : B \underset{1-1}{⟶} P \to I : B \underset{1-1 onto}{⟶} ran I$
44	41 42 43	3syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to I : B \underset{1-1 onto}{⟶} ran I$
45		f1ocnvdm	$⊢ (I : B \underset{1-1 onto}{⟶} ran I \land p \in ran I) \to I^{-1} (p) \in B$
46	44 33 45	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to I^{-1} (p) \in B$
47	46	adantr	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to I^{-1} (p) \in B$
48		simplrl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to S \subseteq B$
49	48	sselda	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to x \in B$
50	1 2 6 7	dihord	$⊢ ((K \in HL \land W \in H) \land I^{-1} (p) \in B \land x \in B) \to (I (I^{-1} (p)) \subseteq I (x) \leftrightarrow I^{-1} (p) \underset{˙}{\leq} x)$
51	40 47 49 50	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to (I (I^{-1} (p)) \subseteq I (x) \leftrightarrow I^{-1} (p) \underset{˙}{\leq} x)$
52	41 33 35	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to I (I^{-1} (p)) = p$
53	52	adantr	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to I (I^{-1} (p)) = p$
54	53	sseq1d	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to (I (I^{-1} (p)) \subseteq I (x) \leftrightarrow p \subseteq I (x))$
55	51 54	bitr3d	$⊢ ((((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \land x \in S) \to (I^{-1} (p) \underset{˙}{\leq} x \leftrightarrow p \subseteq I (x))$
56	55	ralbidva	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D) \to (\forall x \in S I^{-1} (p) \underset{˙}{\leq} x \leftrightarrow \forall x \in S p \subseteq I (x))$
57	56	3adant3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to (\forall x \in S I^{-1} (p) \underset{˙}{\leq} x \leftrightarrow \forall x \in S p \subseteq I (x))$
58	39 57	mpbird	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to \forall x \in S I^{-1} (p) \underset{˙}{\leq} x$
59		simp1ll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to K \in HL$
60	59 19	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to K \in CLat$
61	46	3adant3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to I^{-1} (p) \in B$
62		simp1rl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to S \subseteq B$
63	1 2 5	clatleglb	$⊢ (K \in CLat \land I^{-1} (p) \in B \land S \subseteq B) \to (I^{-1} (p) \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S I^{-1} (p) \underset{˙}{\leq} x)$
64	60 61 62 63	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to (I^{-1} (p) \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S I^{-1} (p) \underset{˙}{\leq} x)$
65	58 64	mpbird	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to I^{-1} (p) \underset{˙}{\leq} G (S)$
66	60 62 22	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to G (S) \in B$
67	1 2 6 7	dihord	$⊢ ((K \in HL \land W \in H) \land I^{-1} (p) \in B \land G (S) \in B) \to (I (I^{-1} (p)) \subseteq I (G (S)) \leftrightarrow I^{-1} (p) \underset{˙}{\leq} G (S))$
68	31 61 66 67	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to (I (I^{-1} (p)) \subseteq I (G (S)) \leftrightarrow I^{-1} (p) \underset{˙}{\leq} G (S))$
69	65 68	mpbird	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to I (I^{-1} (p)) \subseteq I (G (S))$
70	36 69	eqsstrrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to p \subseteq I (G (S))$
71		simp3r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to \neg p \subseteq I (G (S))$
72	70 71	pm2.21fal	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \land p \in D \land (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S)))) \to ⊥$
73	72	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to (\exists p \in D (p \subseteq ⋂_{x \in S} I (x) \land \neg p \subseteq I (G (S))) \to ⊥)$
74	30 73	syld	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to (I (G (S)) \subset ⋂_{x \in S} I (x) \to ⊥)$
75	15 74	mtoi	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to \neg I (G (S)) \subset ⋂_{x \in S} I (x)$
76		dfpss3	$⊢ I (G (S)) \subset ⋂_{x \in S} I (x) \leftrightarrow (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land \neg ⋂_{x \in S} I (x) \subseteq I (G (S)))$
77	76	notbii	$⊢ \neg I (G (S)) \subset ⋂_{x \in S} I (x) \leftrightarrow \neg (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land \neg ⋂_{x \in S} I (x) \subseteq I (G (S)))$
78		iman	$⊢ (I (G (S)) \subseteq ⋂_{x \in S} I (x) \to ⋂_{x \in S} I (x) \subseteq I (G (S))) \leftrightarrow \neg (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land \neg ⋂_{x \in S} I (x) \subseteq I (G (S)))$
79		anclb	$⊢ (I (G (S)) \subseteq ⋂_{x \in S} I (x) \to ⋂_{x \in S} I (x) \subseteq I (G (S))) \leftrightarrow (I (G (S)) \subseteq ⋂_{x \in S} I (x) \to (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land ⋂_{x \in S} I (x) \subseteq I (G (S))))$
80	77 78 79	3bitr2i	$⊢ \neg I (G (S)) \subset ⋂_{x \in S} I (x) \leftrightarrow (I (G (S)) \subseteq ⋂_{x \in S} I (x) \to (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land ⋂_{x \in S} I (x) \subseteq I (G (S))))$
81	75 80	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to (I (G (S)) \subseteq ⋂_{x \in S} I (x) \to (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land ⋂_{x \in S} I (x) \subseteq I (G (S))))$
82	14 81	mpd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land ⋂_{x \in S} I (x) \subseteq I (G (S)))$
83		eqss	$⊢ I (G (S)) = ⋂_{x \in S} I (x) \leftrightarrow (I (G (S)) \subseteq ⋂_{x \in S} I (x) \land ⋂_{x \in S} I (x) \subseteq I (G (S)))$
84	82 83	sylibr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Metamath Proof Explorer

Theorem dihglblem6

Proof