dicn0

Description: The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014)

	Ref	Expression
Hypotheses	dicn0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicn0.a	$⊢ A = Atoms (K)$
	dicn0.h	$⊢ H = LHyp (K)$
	dicn0.i	$⊢ I = DIsoC (K) (W)$
Assertion	dicn0	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		dicn0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicn0.a	$⊢ A = Atoms (K)$
3		dicn0.h	$⊢ H = LHyp (K)$
4		dicn0.i	$⊢ I = DIsoC (K) (W)$
5		simpl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
6		eqid	$⊢ oc (K) = oc (K)$
7	1 6 2 3	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
8	7	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
9		simpr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
10		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
11		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)$
12	1 2 3 10 11	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
13	5 8 9 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W)$
14		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	14 15	tendo02	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q) \in LTrn (K) (W) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = {I ↾}_{{Base}_{K}}$
17	13 16	syl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) = {I ↾}_{{Base}_{K}}$
18	17	eqcomd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to {I ↾}_{{Base}_{K}} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q))$
19		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
20	15 3 10 19 14	tendo0cl	$⊢ (K \in HL \land W \in H) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W)$
21	20	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W)$
22		eqid	$⊢ oc (K) (W) = oc (K) (W)$
23		fvex	$⊢ {Base}_{K} \in V$
24		resiexg	$⊢ {Base}_{K} \in V \to {I ↾}_{{Base}_{K}} \in V$
25	23 24	ax-mp	$⊢ {I ↾}_{{Base}_{K}} \in V$
26		fvex	$⊢ LTrn (K) (W) \in V$
27	26	mptex	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in V$
28	1 2 3 22 10 19 4 25 27	dicopelval	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \in I (Q) \leftrightarrow ({I ↾}_{{Base}_{K}} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = Q)) \land (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W)))$
29	18 21 28	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \in I (Q)$
30	29	ne0d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) \neq \emptyset$

Metamath Proof Explorer

Theorem dicn0

Proof