dih1dimb2

Description: Isomorphism H at an atom under W . (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimb2.b	$⊢ B = {Base}_{K}$
	dih1dimb2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dih1dimb2.a	$⊢ A = Atoms (K)$
	dih1dimb2.h	$⊢ H = LHyp (K)$
	dih1dimb2.t	$⊢ T = LTrn (K) (W)$
	dih1dimb2.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dih1dimb2.u	$⊢ U = DVecH (K) (W)$
	dih1dimb2.i	$⊢ I = DIsoH (K) (W)$
	dih1dimb2.n	$⊢ N = LSpan (U)$
Assertion	dih1dimb2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to \exists f \in T (f \neq {I ↾}_{B} \land I (Q) = N (\{⟨f, O⟩\}))$

Proof

Step	Hyp	Ref	Expression
1		dih1dimb2.b	$⊢ B = {Base}_{K}$
2		dih1dimb2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dih1dimb2.a	$⊢ A = Atoms (K)$
4		dih1dimb2.h	$⊢ H = LHyp (K)$
5		dih1dimb2.t	$⊢ T = LTrn (K) (W)$
6		dih1dimb2.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		dih1dimb2.u	$⊢ U = DVecH (K) (W)$
8		dih1dimb2.i	$⊢ I = DIsoH (K) (W)$
9		dih1dimb2.n	$⊢ N = LSpan (U)$
10		eqid	$⊢ trL (K) (W) = trL (K) (W)$
11	2 3 4 5 10	cdlemf	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to \exists f \in T trL (K) (W) (f) = Q$
12		simp3	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to trL (K) (W) (f) = Q$
13		simp1rl	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to Q \in A$
14	12 13	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to trL (K) (W) (f) \in A$
15		simp1l	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to (K \in HL \land W \in H)$
16		simp2	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to f \in T$
17	1 3 4 5 10	trlnidatb	$⊢ ((K \in HL \land W \in H) \land f \in T) \to (f \neq {I ↾}_{B} \leftrightarrow trL (K) (W) (f) \in A)$
18	15 16 17	syl2anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to (f \neq {I ↾}_{B} \leftrightarrow trL (K) (W) (f) \in A)$
19	14 18	mpbird	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to f \neq {I ↾}_{B}$
20	12	fveq2d	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to I (trL (K) (W) (f)) = I (Q)$
21	1 4 5 10 6 7 8 9	dih1dimb	$⊢ ((K \in HL \land W \in H) \land f \in T) \to I (trL (K) (W) (f)) = N (\{⟨f, O⟩\})$
22	15 16 21	syl2anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to I (trL (K) (W) (f)) = N (\{⟨f, O⟩\})$
23	20 22	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to I (Q) = N (\{⟨f, O⟩\})$
24	19 23	jca	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T \land trL (K) (W) (f) = Q) \to (f \neq {I ↾}_{B} \land I (Q) = N (\{⟨f, O⟩\}))$
25	24	3expia	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land f \in T) \to (trL (K) (W) (f) = Q \to (f \neq {I ↾}_{B} \land I (Q) = N (\{⟨f, O⟩\})))$
26	25	reximdva	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to (\exists f \in T trL (K) (W) (f) = Q \to \exists f \in T (f \neq {I ↾}_{B} \land I (Q) = N (\{⟨f, O⟩\})))$
27	11 26	mpd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to \exists f \in T (f \neq {I ↾}_{B} \land I (Q) = N (\{⟨f, O⟩\}))$

Metamath Proof Explorer

Theorem dih1dimb2

Proof