dihwN

Description: Value of isomorphism H at the fiducial hyperplane W . (Contributed by NM, 25-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihw.b	$⊢ B = {Base}_{K}$
	dihw.h	$⊢ H = LHyp (K)$
	dihw.t	$⊢ T = LTrn (K) (W)$
	dihw.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	dihw.i	$⊢ I = DIsoH (K) (W)$
	dihw.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	dihwN	$⊢ φ \to I (W) = T \times \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		dihw.b	$⊢ B = {Base}_{K}$
2		dihw.h	$⊢ H = LHyp (K)$
3		dihw.t	$⊢ T = LTrn (K) (W)$
4		dihw.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
5		dihw.i	$⊢ I = DIsoH (K) (W)$
6		dihw.k	$⊢ φ \to (K \in HL \land W \in H)$
7	6	simprd	$⊢ φ \to W \in H$
8	1 2	lhpbase	$⊢ W \in H \to W \in B$
9	7 8	syl	$⊢ φ \to W \in B$
10	6	simpld	$⊢ φ \to K \in HL$
11	10	hllatd	$⊢ φ \to K \in Lat$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13	1 12	latref	$⊢ (K \in Lat \land W \in B) \to W \leq_{K} W$
14	11 9 13	syl2anc	$⊢ φ \to W \leq_{K} W$
15	9 14	jca	$⊢ φ \to (W \in B \land W \leq_{K} W)$
16		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
17	1 12 2 5 16	dihvalb	$⊢ ((K \in HL \land W \in H) \land (W \in B \land W \leq_{K} W)) \to I (W) = DIsoB (K) (W) (W)$
18	6 15 17	syl2anc	$⊢ φ \to I (W) = DIsoB (K) (W) (W)$
19		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
20	1 12 2 3 4 19 16	dibval2	$⊢ ((K \in HL \land W \in H) \land (W \in B \land W \leq_{K} W)) \to DIsoB (K) (W) (W) = DIsoA (K) (W) (W) \times \{\underset{˙}{0}\}$
21	6 15 20	syl2anc	$⊢ φ \to DIsoB (K) (W) (W) = DIsoA (K) (W) (W) \times \{\underset{˙}{0}\}$
22		eqid	$⊢ trL (K) (W) = trL (K) (W)$
23	1 12 2 3 22 19	diaval	$⊢ ((K \in HL \land W \in H) \land (W \in B \land W \leq_{K} W)) \to DIsoA (K) (W) (W) = \{g \in T \| trL (K) (W) (g) \leq_{K} W\}$
24	6 15 23	syl2anc	$⊢ φ \to DIsoA (K) (W) (W) = \{g \in T \| trL (K) (W) (g) \leq_{K} W\}$
25	12 2 3 22	trlle	$⊢ ((K \in HL \land W \in H) \land g \in T) \to trL (K) (W) (g) \leq_{K} W$
26	6 25	sylan	$⊢ (φ \land g \in T) \to trL (K) (W) (g) \leq_{K} W$
27	26	ralrimiva	$⊢ φ \to \forall g \in T trL (K) (W) (g) \leq_{K} W$
28		rabid2	$⊢ T = \{g \in T \| trL (K) (W) (g) \leq_{K} W\} \leftrightarrow \forall g \in T trL (K) (W) (g) \leq_{K} W$
29	27 28	sylibr	$⊢ φ \to T = \{g \in T \| trL (K) (W) (g) \leq_{K} W\}$
30	24 29	eqtr4d	$⊢ φ \to DIsoA (K) (W) (W) = T$
31	30	xpeq1d	$⊢ φ \to DIsoA (K) (W) (W) \times \{\underset{˙}{0}\} = T \times \{\underset{˙}{0}\}$
32	18 21 31	3eqtrd	$⊢ φ \to I (W) = T \times \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dihwN

Proof