dicelval2nd

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

	Ref	Expression
Hypotheses	dicelval2nd.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicelval2nd.a	$⊢ A = Atoms (K)$
	dicelval2nd.h	$⊢ H = LHyp (K)$
	dicelval2nd.e	$⊢ E = TEndo (K) (W)$
	dicelval2nd.i	$⊢ I = DIsoC (K) (W)$
Assertion	dicelval2nd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 2^{nd} (Y) \in E$

Step	Hyp	Ref	Expression
1		dicelval2nd.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicelval2nd.a	$⊢ A = Atoms (K)$
3		dicelval2nd.h	$⊢ H = LHyp (K)$
4		dicelval2nd.e	$⊢ E = TEndo (K) (W)$
5		dicelval2nd.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	$⊢ LTrn (K) (W) = LTrn (K) (W)$
10	3 9 4 6 7	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{DVecH (K) (W)} = LTrn (K) (W) \times E$
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)} = LTrn (K) (W) \times E$
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 LTrn (K) (W) \times E$
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 (LTrn (K) (W) \times E))$
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 (LTrn (K) (W) \times E)$
15		xp2nd	$⊢ Y \in (LTrn (K) (W) \times E) \to 2^{nd} (Y) \in E$
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 2^{nd} (Y) \in E$

Metamath Proof Explorer