Metamath Proof Explorer

Theorem dicelval1sta

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

		Ref	Expression
	Hypotheses	dicelval1sta.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		dicelval1sta.a	$⊢ A = Atoms (K)$
		dicelval1sta.h	$⊢ H = LHyp (K)$
		dicelval1sta.p	$⊢ P = oc (K) (W)$
		dicelval1sta.t	$⊢ T = LTrn (K) (W)$
		dicelval1sta.i	$⊢ I = DIsoC (K) (W)$
	Assertion	dicelval1sta	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q))$

Proof

Step	Hyp	Ref	Expression
1		dicelval1sta.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicelval1sta.a	$⊢ A = Atoms (K)$
3		dicelval1sta.h	$⊢ H = LHyp (K)$
4		dicelval1sta.p	$⊢ P = oc (K) (W)$
5		dicelval1sta.t	$⊢ T = LTrn (K) (W)$
6		dicelval1sta.i	$⊢ I = DIsoC (K) (W)$
7		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
8	1 2 3 4 5 7 6	dicval	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W))\}$
9	8	eleq2d	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow Y \in \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W))\})$
10	9	biimp3a	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to Y \in \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W))\}$
11		eqeq1	$⊢ f = 1^{st} (Y) \to (f = s ((ι g \in T \| g (P) = Q)) \leftrightarrow 1^{st} (Y) = s ((ι g \in T \| g (P) = Q)))$
12	11	anbi1d	$⊢ f = 1^{st} (Y) \to ((f = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W)) \leftrightarrow (1^{st} (Y) = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W)))$
13		fveq1	$⊢ s = 2^{nd} (Y) \to s ((ι g \in T \| g (P) = Q)) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q))$
14	13	eqeq2d	$⊢ s = 2^{nd} (Y) \to (1^{st} (Y) = s ((ι g \in T \| g (P) = Q)) \leftrightarrow 1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)))$
15		eleq1	$⊢ s = 2^{nd} (Y) \to (s \in TEndo (K) (W) \leftrightarrow 2^{nd} (Y) \in TEndo (K) (W))$
16	14 15	anbi12d	$⊢ s = 2^{nd} (Y) \to ((1^{st} (Y) = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W)) \leftrightarrow (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in TEndo (K) (W)))$
17	12 16	elopabi	$⊢ Y \in \{⟨f, s⟩ \| (f = s ((ι g \in T \| g (P) = Q)) \land s \in TEndo (K) (W))\} \to (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in TEndo (K) (W))$
18	10 17	syl	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in TEndo (K) (W))$
19	18	simpld	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land Y \in I (Q)) \to 1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q))$