dihmeetlem2N

Description: Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem2.b	$⊢ B = {Base}_{K}$
	dihmeetlem2.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem2.h	$⊢ H = LHyp (K)$
	dihmeetlem2.i	$⊢ I = DIsoH (K) (W)$
	dihmeetlem2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem2.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem2.a	$⊢ A = Atoms (K)$
	dihmeetlem2.p	$⊢ P = oc (K) (W)$
	dihmeetlem2.t	$⊢ T = LTrn (K) (W)$
	dihmeetlem2.r	$⊢ R = trL (K) (W)$
	dihmeetlem2.e	$⊢ E = TEndo (K) (W)$
	dihmeetlem2.g	$⊢ G = (ι h \in T \| h (P) = q)$
	dihmeetlem2.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
Assertion	dihmeetlem2N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Proof

Step	Hyp	Ref	Expression
1		dihmeetlem2.b	$⊢ B = {Base}_{K}$
2		dihmeetlem2.m	$⊢ \underset{˙}{\land} = meet (K)$
3		dihmeetlem2.h	$⊢ H = LHyp (K)$
4		dihmeetlem2.i	$⊢ I = DIsoH (K) (W)$
5		dihmeetlem2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		dihmeetlem2.j	$⊢ \underset{˙}{\lor} = join (K)$
7		dihmeetlem2.a	$⊢ A = Atoms (K)$
8		dihmeetlem2.p	$⊢ P = oc (K) (W)$
9		dihmeetlem2.t	$⊢ T = LTrn (K) (W)$
10		dihmeetlem2.r	$⊢ R = trL (K) (W)$
11		dihmeetlem2.e	$⊢ E = TEndo (K) (W)$
12		dihmeetlem2.g	$⊢ G = (ι h \in T \| h (P) = q)$
13		dihmeetlem2.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
14		eqid	$⊢ glb (K) = glb (K)$
15		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in HL$
16		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in B$
17		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in B$
18	14 2 15 16 17	meetval	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
19	18	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to DIsoB (K) (W) (X \underset{˙}{\land} Y) = DIsoB (K) (W) (glb (K) (\{X, Y\}))$
20		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
21		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
22	1 5 3 21	dibeldmN	$⊢ (K \in HL \land W \in H) \to (X \in dom DIsoB (K) (W) \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$
23	22	biimpar	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \in dom DIsoB (K) (W)$
24	23	3adant3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in dom DIsoB (K) (W)$
25	1 5 3 21	dibeldmN	$⊢ (K \in HL \land W \in H) \to (Y \in dom DIsoB (K) (W) \leftrightarrow (Y \in B \land Y \underset{˙}{\leq} W))$
26	25	biimpar	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in dom DIsoB (K) (W)$
27	26	3adant2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in dom DIsoB (K) (W)$
28		prssg	$⊢ (X \in B \land Y \in B) \to ((X \in dom DIsoB (K) (W) \land Y \in dom DIsoB (K) (W)) \leftrightarrow \{X, Y\} \subseteq dom DIsoB (K) (W))$
29	16 17 28	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((X \in dom DIsoB (K) (W) \land Y \in dom DIsoB (K) (W)) \leftrightarrow \{X, Y\} \subseteq dom DIsoB (K) (W))$
30	24 27 29	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to \{X, Y\} \subseteq dom DIsoB (K) (W)$
31		prnzg	$⊢ X \in B \to \{X, Y\} \neq \emptyset$
32	16 31	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to \{X, Y\} \neq \emptyset$
33	14 3 21	dibglbN	$⊢ ((K \in HL \land W \in H) \land (\{X, Y\} \subseteq dom DIsoB (K) (W) \land \{X, Y\} \neq \emptyset)) \to DIsoB (K) (W) (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} DIsoB (K) (W) (x)$
34	20 30 32 33	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to DIsoB (K) (W) (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} DIsoB (K) (W) (x)$
35	19 34	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to DIsoB (K) (W) (X \underset{˙}{\land} Y) = ⋂_{x \in \{X, Y\}} DIsoB (K) (W) (x)$
36	15	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in Lat$
37	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
38	36 16 17 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\land} Y \in B$
39		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to W \in H$
40	1 3	lhpbase	$⊢ W \in H \to W \in B$
41	39 40	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to W \in B$
42	1 5 2	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
43	36 16 17 42	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
44		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\leq} W$
45	1 5 36 38 16 41 43 44	lattrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
46	1 5 3 4 21	dihvalb	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = DIsoB (K) (W) (X \underset{˙}{\land} Y)$
47	20 38 45 46	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = DIsoB (K) (W) (X \underset{˙}{\land} Y)$
48		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x \in \{X, Y\}) \to (K \in HL \land W \in H)$
49		vex	$⊢ x \in V$
50	49	elpr	$⊢ x \in \{X, Y\} \leftrightarrow (x = X \lor x = Y)$
51		simpl2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = X) \to (X \in B \land X \underset{˙}{\leq} W)$
52		eleq1	$⊢ x = X \to (x \in B \leftrightarrow X \in B)$
53		breq1	$⊢ x = X \to (x \underset{˙}{\leq} W \leftrightarrow X \underset{˙}{\leq} W)$
54	52 53	anbi12d	$⊢ x = X \to ((x \in B \land x \underset{˙}{\leq} W) \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$
55	54	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = X) \to ((x \in B \land x \underset{˙}{\leq} W) \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$
56	51 55	mpbird	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = X) \to (x \in B \land x \underset{˙}{\leq} W)$
57		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = Y) \to (Y \in B \land Y \underset{˙}{\leq} W)$
58		eleq1	$⊢ x = Y \to (x \in B \leftrightarrow Y \in B)$
59		breq1	$⊢ x = Y \to (x \underset{˙}{\leq} W \leftrightarrow Y \underset{˙}{\leq} W)$
60	58 59	anbi12d	$⊢ x = Y \to ((x \in B \land x \underset{˙}{\leq} W) \leftrightarrow (Y \in B \land Y \underset{˙}{\leq} W))$
61	60	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = Y) \to ((x \in B \land x \underset{˙}{\leq} W) \leftrightarrow (Y \in B \land Y \underset{˙}{\leq} W))$
62	57 61	mpbird	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x = Y) \to (x \in B \land x \underset{˙}{\leq} W)$
63	56 62	jaodan	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (x = X \lor x = Y)) \to (x \in B \land x \underset{˙}{\leq} W)$
64	50 63	sylan2b	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x \in \{X, Y\}) \to (x \in B \land x \underset{˙}{\leq} W)$
65	1 5 3 4 21	dihvalb	$⊢ ((K \in HL \land W \in H) \land (x \in B \land x \underset{˙}{\leq} W)) \to I (x) = DIsoB (K) (W) (x)$
66	48 64 65	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land x \in \{X, Y\}) \to I (x) = DIsoB (K) (W) (x)$
67	66	iineq2dv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ⋂_{x \in \{X, Y\}} I (x) = ⋂_{x \in \{X, Y\}} DIsoB (K) (W) (x)$
68	35 47 67	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = ⋂_{x \in \{X, Y\}} I (x)$
69		fveq2	$⊢ x = X \to I (x) = I (X)$
70		fveq2	$⊢ x = Y \to I (x) = I (Y)$
71	69 70	iinxprg	$⊢ (X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
72	16 17 71	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
73	68 72	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetlem2N

Proof