dib0

Description: The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014)

	Ref	Expression
Hypotheses	dib0.z	$⊢ \underset{˙}{0} = 0. (K)$
	dib0.h	$⊢ H = LHyp (K)$
	dib0.i	$⊢ I = DIsoB (K) (W)$
	dib0.u	$⊢ U = DVecH (K) (W)$
	dib0.o	$⊢ O = 0_{U}$
Assertion	dib0	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = \{O\}$

Proof

Step	Hyp	Ref	Expression
1		dib0.z	$⊢ \underset{˙}{0} = 0. (K)$
2		dib0.h	$⊢ H = LHyp (K)$
3		dib0.i	$⊢ I = DIsoB (K) (W)$
4		dib0.u	$⊢ U = DVecH (K) (W)$
5		dib0.o	$⊢ O = 0_{U}$
6		fvex	$⊢ {Base}_{K} \in V$
7		resiexg	$⊢ {Base}_{K} \in V \to {I ↾}_{{Base}_{K}} \in V$
8	6 7	ax-mp	$⊢ {I ↾}_{{Base}_{K}} \in V$
9		fvex	$⊢ LTrn (K) (W) \in V$
10	9	mptex	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in V$
11	8 10	xpsn	$⊢ \{{I ↾}_{{Base}_{K}}\} \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\} = \{⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}$
12		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
13		hlop	$⊢ K \in HL \to K \in OP$
14	13	adantr	$⊢ (K \in HL \land W \in H) \to K \in OP$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 1	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
17	14 16	syl	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \in {Base}_{K}$
18	15 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	15 19 1	op0le	$⊢ (K \in OP \land W \in {Base}_{K}) \to \underset{˙}{0} \leq_{K} W$
21	13 18 20	syl2an	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \leq_{K} W$
22		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
23		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
24		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
25	15 19 2 22 23 24 3	dibval2	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{0} \in {Base}_{K} \land \underset{˙}{0} \leq_{K} W)) \to I (\underset{˙}{0}) = DIsoA (K) (W) (\underset{˙}{0}) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
26	12 17 21 25	syl12anc	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = DIsoA (K) (W) (\underset{˙}{0}) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
27	15 1 2 24	dia0	$⊢ (K \in HL \land W \in H) \to DIsoA (K) (W) (\underset{˙}{0}) = \{{I ↾}_{{Base}_{K}}\}$
28	27	xpeq1d	$⊢ (K \in HL \land W \in H) \to DIsoA (K) (W) (\underset{˙}{0}) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\} = \{{I ↾}_{{Base}_{K}}\} \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
29	26 28	eqtrd	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = \{{I ↾}_{{Base}_{K}}\} \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
30	15 2 22 4 5 23	dvh0g	$⊢ (K \in HL \land W \in H) \to O = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
31	30	sneqd	$⊢ (K \in HL \land W \in H) \to \{O\} = \{⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}$
32	11 29 31	3eqtr4a	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = \{O\}$

Metamath Proof Explorer

Theorem dib0

Proof