dihglblem5aN

Description: A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem5a.b	$⊢ B = {Base}_{K}$
	dihglblem5a.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglblem5a.h	$⊢ H = LHyp (K)$
	dihglblem5a.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihglblem5aN	$⊢ ((K \in HL \land W \in H) \land X \in B) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$

Proof

Step	Hyp	Ref	Expression
1		dihglblem5a.b	$⊢ B = {Base}_{K}$
2		dihglblem5a.m	$⊢ \underset{˙}{\land} = meet (K)$
3		dihglblem5a.h	$⊢ H = LHyp (K)$
4		dihglblem5a.i	$⊢ I = DIsoH (K) (W)$
5		simpr	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to X \leq_{K} W$
6		hllat	$⊢ K \in HL \to K \in Lat$
7	6	ad3antrrr	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to K \in Lat$
8		simplr	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to X \in B$
9	1 3	lhpbase	$⊢ W \in H \to W \in B$
10	9	ad3antlr	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to W \in B$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	1 11 2	latleeqm1	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \leq_{K} W \leftrightarrow X \underset{˙}{\land} W = X)$
13	7 8 10 12	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to (X \leq_{K} W \leftrightarrow X \underset{˙}{\land} W = X)$
14	5 13	mpbid	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to X \underset{˙}{\land} W = X$
15	14	fveq2d	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to I (X \underset{˙}{\land} W) = I (X)$
16		simpll	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to (K \in HL \land W \in H)$
17	1 11 3 4	dihord	$⊢ ((K \in HL \land W \in H) \land X \in B \land W \in B) \to (I (X) \subseteq I (W) \leftrightarrow X \leq_{K} W)$
18	16 8 10 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to (I (X) \subseteq I (W) \leftrightarrow X \leq_{K} W)$
19	5 18	mpbird	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to I (X) \subseteq I (W)$
20		df-ss	$⊢ I (X) \subseteq I (W) \leftrightarrow I (X) \cap I (W) = I (X)$
21	19 20	sylib	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to I (X) \cap I (W) = I (X)$
22	15 21	eqtr4d	$⊢ (((K \in HL \land W \in H) \land X \in B) \land X \leq_{K} W) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$
23		eqid	$⊢ join (K) = join (K)$
24		eqid	$⊢ Atoms (K) = Atoms (K)$
25		eqid	$⊢ oc (K) (W) = oc (K) (W)$
26		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
27		eqid	$⊢ trL (K) (W) = trL (K) (W)$
28		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
29		eqid	$⊢ (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = q) = (ι h \in LTrn (K) (W) \| h (oc (K) (W)) = q)$
30		eqid	$⊢ (h \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{B})$
31	1 2 3 4 11 23 24 25 26 27 28 29 30	dihglblem5apreN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \leq_{K} W)) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$
32	31	anassrs	$⊢ (((K \in HL \land W \in H) \land X \in B) \land \neg X \leq_{K} W) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$
33	22 32	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land X \in B) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$

Metamath Proof Explorer

Theorem dihglblem5aN

Proof