diaglbN

Description: Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	diaglb.g	$⊢ G = glb (K)$
	diaglb.h	$⊢ H = LHyp (K)$
	diaglb.i	$⊢ I = DIsoA (K) (W)$
Assertion	diaglbN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Proof

Step	Hyp	Ref	Expression
1		diaglb.g	$⊢ G = glb (K)$
2		diaglb.h	$⊢ H = LHyp (K)$
3		diaglb.i	$⊢ I = DIsoA (K) (W)$
4		simpl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (K \in HL \land W \in H)$
5		hlclat	$⊢ K \in HL \to K \in CLat$
6	5	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to K \in CLat$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	7 8 2 3	diadm	$⊢ (K \in HL \land W \in H) \to dom I = \{y \in {Base}_{K} \| y \leq_{K} W\}$
10	9	sseq2d	$⊢ (K \in HL \land W \in H) \to (S \subseteq dom I \leftrightarrow S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\})$
11	10	biimpa	$⊢ ((K \in HL \land W \in H) \land S \subseteq dom I) \to S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\}$
12	11	adantrr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \subseteq \{y \in {Base}_{K} \| y \leq_{K} W\}$
13		ssrab2	$⊢ \{y \in {Base}_{K} \| y \leq_{K} W\} \subseteq {Base}_{K}$
14	12 13	sstrdi	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \subseteq {Base}_{K}$
15	7 1	clatglbcl	$⊢ (K \in CLat \land S \subseteq {Base}_{K}) \to G (S) \in {Base}_{K}$
16	6 14 15	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to G (S) \in {Base}_{K}$
17		simprr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to S \neq \emptyset$
18		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
19	17 18	sylib	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to \exists x x \in S$
20		hllat	$⊢ K \in HL \to K \in Lat$
21	20	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to K \in Lat$
22	16	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to G (S) \in {Base}_{K}$
23		ssel2	$⊢ (S \subseteq dom I \land x \in S) \to x \in dom I$
24	23	adantlr	$⊢ ((S \subseteq dom I \land S \neq \emptyset) \land x \in S) \to x \in dom I$
25	24	adantll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to x \in dom I$
26	7 8 2 3	diaeldm	$⊢ (K \in HL \land W \in H) \to (x \in dom I \leftrightarrow (x \in {Base}_{K} \land x \leq_{K} W))$
27	26	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to (x \in dom I \leftrightarrow (x \in {Base}_{K} \land x \leq_{K} W))$
28	25 27	mpbid	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to (x \in {Base}_{K} \land x \leq_{K} W)$
29	28	simpld	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to x \in {Base}_{K}$
30	7 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
31	30	ad3antlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to W \in {Base}_{K}$
32	5	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to K \in CLat$
33	14	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to S \subseteq {Base}_{K}$
34		simpr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to x \in S$
35	7 8 1	clatglble	$⊢ (K \in CLat \land S \subseteq {Base}_{K} \land x \in S) \to G (S) \leq_{K} x$
36	32 33 34 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to G (S) \leq_{K} x$
37	28	simprd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to x \leq_{K} W$
38	7 8 21 22 29 31 36 37	lattrd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to G (S) \leq_{K} W$
39	19 38	exlimddv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to G (S) \leq_{K} W$
40		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
41		eqid	$⊢ trL (K) (W) = trL (K) (W)$
42	7 8 2 40 41 3	diaelval	$⊢ ((K \in HL \land W \in H) \land (G (S) \in {Base}_{K} \land G (S) \leq_{K} W)) \to (f \in I (G (S)) \leftrightarrow (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} G (S)))$
43	4 16 39 42	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (f \in I (G (S)) \leftrightarrow (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} G (S)))$
44		r19.28zv	$⊢ S \neq \emptyset \to (\forall x \in S (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} x) \leftrightarrow (f \in LTrn (K) (W) \land \forall x \in S trL (K) (W) (f) \leq_{K} x))$
45	44	ad2antll	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (\forall x \in S (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} x) \leftrightarrow (f \in LTrn (K) (W) \land \forall x \in S trL (K) (W) (f) \leq_{K} x))$
46		simpll	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to (K \in HL \land W \in H)$
47	7 8 2 40 41 3	diaelval	$⊢ ((K \in HL \land W \in H) \land (x \in {Base}_{K} \land x \leq_{K} W)) \to (f \in I (x) \leftrightarrow (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} x))$
48	46 28 47	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land x \in S) \to (f \in I (x) \leftrightarrow (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} x))$
49	48	ralbidva	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (\forall x \in S f \in I (x) \leftrightarrow \forall x \in S (f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} x))$
50	5	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land f \in LTrn (K) (W)) \to K \in CLat$
51	7 2 40 41	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in LTrn (K) (W)) \to trL (K) (W) (f) \in {Base}_{K}$
52	51	adantlr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land f \in LTrn (K) (W)) \to trL (K) (W) (f) \in {Base}_{K}$
53	14	adantr	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land f \in LTrn (K) (W)) \to S \subseteq {Base}_{K}$
54	7 8 1	clatleglb	$⊢ (K \in CLat \land trL (K) (W) (f) \in {Base}_{K} \land S \subseteq {Base}_{K}) \to (trL (K) (W) (f) \leq_{K} G (S) \leftrightarrow \forall x \in S trL (K) (W) (f) \leq_{K} x)$
55	50 52 53 54	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \land f \in LTrn (K) (W)) \to (trL (K) (W) (f) \leq_{K} G (S) \leftrightarrow \forall x \in S trL (K) (W) (f) \leq_{K} x)$
56	55	pm5.32da	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to ((f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} G (S)) \leftrightarrow (f \in LTrn (K) (W) \land \forall x \in S trL (K) (W) (f) \leq_{K} x))$
57	45 49 56	3bitr4rd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to ((f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} G (S)) \leftrightarrow \forall x \in S f \in I (x))$
58		vex	$⊢ f \in V$
59		eliin	$⊢ f \in V \to (f \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S f \in I (x))$
60	58 59	ax-mp	$⊢ f \in ⋂_{x \in S} I (x) \leftrightarrow \forall x \in S f \in I (x)$
61	57 60	syl6bbr	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to ((f \in LTrn (K) (W) \land trL (K) (W) (f) \leq_{K} G (S)) \leftrightarrow f \in ⋂_{x \in S} I (x))$
62	43 61	bitrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to (f \in I (G (S)) \leftrightarrow f \in ⋂_{x \in S} I (x))$
63	62	eqrdv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq dom I \land S \neq \emptyset)) \to I (G (S)) = ⋂_{x \in S} I (x)$

Metamath Proof Explorer

Theorem diaglbN

Proof