dibfval

Description: The partial isomorphism B for a lattice K . (Contributed by NM, 8-Dec-2013)

	Ref	Expression
Hypotheses	dibval.b	$⊢ B = {Base}_{K}$
	dibval.h	$⊢ H = LHyp (K)$
	dibval.t	$⊢ T = LTrn (K) (W)$
	dibval.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	dibval.j	$⊢ J = DIsoA (K) (W)$
	dibval.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibfval	$⊢ (K \in V \land W \in H) \to I = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		dibval.b	$⊢ B = {Base}_{K}$
2		dibval.h	$⊢ H = LHyp (K)$
3		dibval.t	$⊢ T = LTrn (K) (W)$
4		dibval.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
5		dibval.j	$⊢ J = DIsoA (K) (W)$
6		dibval.i	$⊢ I = DIsoB (K) (W)$
7	1 2	dibffval	$⊢ K \in V \to DIsoB (K) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$
8	7	fveq1d	$⊢ K \in V \to DIsoB (K) (W) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\})) (W)$
9	6 8	syl5eq	$⊢ K \in V \to I = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\})) (W)$
10		fveq2	$⊢ w = W \to DIsoA (K) (w) = DIsoA (K) (W)$
11	10 5	eqtr4di	$⊢ w = W \to DIsoA (K) (w) = J$
12	11	dmeqd	$⊢ w = W \to dom DIsoA (K) (w) = dom J$
13	11	fveq1d	$⊢ w = W \to DIsoA (K) (w) (x) = J (x)$
14		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
15	14 3	eqtr4di	$⊢ w = W \to LTrn (K) (w) = T$
16		eqidd	$⊢ w = W \to {I ↾}_{B} = {I ↾}_{B}$
17	15 16	mpteq12dv	$⊢ w = W \to (f \in LTrn (K) (w) ⟼ {I ↾}_{B}) = (f \in T ⟼ {I ↾}_{B})$
18	17 4	eqtr4di	$⊢ w = W \to (f \in LTrn (K) (w) ⟼ {I ↾}_{B}) = \underset{˙}{0}$
19	18	sneqd	$⊢ w = W \to \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\} = \{\underset{˙}{0}\}$
20	13 19	xpeq12d	$⊢ w = W \to DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\} = J (x) \times \{\underset{˙}{0}\}$
21	12 20	mpteq12dv	$⊢ w = W \to (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}) = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$
22		eqid	$⊢ (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\})) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$
23	5	fvexi	$⊢ J \in V$
24	23	dmex	$⊢ dom J \in V$
25	24	mptex	$⊢ (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\}) \in V$
26	21 22 25	fvmpt	$⊢ W \in H \to (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\})) (W) = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$
27	9 26	sylan9eq	$⊢ (K \in V \land W \in H) \to I = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem dibfval

Proof