Metamath Proof Explorer

Theorem dia1eldmN

Description: The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dia1eldm.h	$⊢ H = LHyp (K)$
		dia1eldm.i	$⊢ I = DIsoA (K) (W)$
	Assertion	dia1eldmN	$⊢ (K \in HL \land W \in H) \to W \in dom I$

Proof

Step	Hyp	Ref	Expression
1		dia1eldm.h	$⊢ H = LHyp (K)$
2		dia1eldm.i	$⊢ I = DIsoA (K) (W)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4	3 1	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
5	4	adantl	$⊢ (K \in HL \land W \in H) \to W \in {Base}_{K}$
6		hllat	$⊢ K \in HL \to K \in Lat$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	3 7	latref	$⊢ (K \in Lat \land W \in {Base}_{K}) \to W \leq_{K} W$
9	6 4 8	syl2an	$⊢ (K \in HL \land W \in H) \to W \leq_{K} W$
10	3 7 1 2	diaeldm	$⊢ (K \in HL \land W \in H) \to (W \in dom I \leftrightarrow (W \in {Base}_{K} \land W \leq_{K} W))$
11	5 9 10	mpbir2and	$⊢ (K \in HL \land W \in H) \to W \in dom I$