dicelval1stN

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 16-Feb-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dicelval1st.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicelval1st.a	$⊢ A = Atoms (K)$
	dicelval1st.h	$⊢ H = LHyp (K)$
	dicelval1st.t	$⊢ T = LTrn (K) (W)$
	dicelval1st.i	$⊢ I = DIsoC (K) (W)$
Assertion	dicelval1stN	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 1^{st} (Y) \in T$

Step	Hyp	Ref	Expression
1		dicelval1st.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicelval1st.a	$⊢ A = Atoms (K)$
3		dicelval1st.h	$⊢ H = LHyp (K)$
4		dicelval1st.t	$⊢ T = LTrn (K) (W)$
5		dicelval1st.i	$⊢ I = DIsoC (K) (W)$
6		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
7		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
8	1 2 3 5 6 7	dicssdvh	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq {Base}_{DVecH (K) (W)}$
9		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
10	3 4 9 6 7	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{DVecH (K) (W)} = T \times TEndo (K) (W)$
11	10	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to {Base}_{DVecH (K) (W)} = T \times TEndo (K) (W)$
12	8 11	sseqtrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \subseteq T \times TEndo (K) (W)$
13	12	sseld	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \to Y \in (T \times TEndo (K) (W)))$
14	13	3impia	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to Y \in (T \times TEndo (K) (W))$
15		xp1st	$⊢ Y \in (T \times TEndo (K) (W)) \to 1^{st} (Y) \in T$
16	14 15	syl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 1^{st} (Y) \in T$

Metamath Proof Explorer