hdmap1eq

Description: The defining equation for h(x,x',y)=y' in part (2) in Baer p. 45 line 24. (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmap1val2.h	$⊢ H = LHyp (K)$
	hdmap1val2.u	$⊢ U = DVecH (K) (W)$
	hdmap1val2.v	$⊢ V = {Base}_{U}$
	hdmap1val2.s	$⊢ \underset{˙}{-} = -_{U}$
	hdmap1val2.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap1val2.n	$⊢ N = LSpan (U)$
	hdmap1val2.c	$⊢ C = LCDual (K) (W)$
	hdmap1val2.d	$⊢ D = {Base}_{C}$
	hdmap1val2.r	$⊢ R = -_{C}$
	hdmap1val2.l	$⊢ L = LSpan (C)$
	hdmap1val2.m	$⊢ M = mapd (K) (W)$
	hdmap1val2.i	$⊢ I = HDMap1 (K) (W)$
	hdmap1val2.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap1eq.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1eq.f	$⊢ φ \to F \in D$
	hdmap1eq.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap1eq.g	$⊢ φ \to G \in D$
	hdmap1eq.e	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	hdmap1eq.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
Assertion	hdmap1eq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})))$

Proof

Step	Hyp	Ref	Expression
1		hdmap1val2.h	$⊢ H = LHyp (K)$
2		hdmap1val2.u	$⊢ U = DVecH (K) (W)$
3		hdmap1val2.v	$⊢ V = {Base}_{U}$
4		hdmap1val2.s	$⊢ \underset{˙}{-} = -_{U}$
5		hdmap1val2.o	$⊢ \underset{˙}{0} = 0_{U}$
6		hdmap1val2.n	$⊢ N = LSpan (U)$
7		hdmap1val2.c	$⊢ C = LCDual (K) (W)$
8		hdmap1val2.d	$⊢ D = {Base}_{C}$
9		hdmap1val2.r	$⊢ R = -_{C}$
10		hdmap1val2.l	$⊢ L = LSpan (C)$
11		hdmap1val2.m	$⊢ M = mapd (K) (W)$
12		hdmap1val2.i	$⊢ I = HDMap1 (K) (W)$
13		hdmap1val2.k	$⊢ φ \to (K \in HL \land W \in H)$
14		hdmap1eq.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
15		hdmap1eq.f	$⊢ φ \to F \in D$
16		hdmap1eq.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
17		hdmap1eq.g	$⊢ φ \to G \in D$
18		hdmap1eq.e	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
19		hdmap1eq.mn	$⊢ φ \to M (N (\{X\})) = L (\{F\})$
20	14	eldifad	$⊢ φ \to X \in V$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 20 15 16	hdmap1val2	$⊢ φ \to I (⟨X, F, Y⟩) = (ι h \in D \| (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\})))$
22	21	eqeq1d	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (ι h \in D \| (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}))) = G)$
23	1 11 2 3 4 5 6 7 8 9 10 13 14 16 15 18 19	mapdpg	$⊢ φ \to \exists! h \in D (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}))$
24		nfv	$⊢ Ⅎ h φ$
25		nfcvd	$⊢ φ \to \underline{Ⅎ} h G$
26		nfvd	$⊢ φ \to Ⅎ h (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\}))$
27		sneq	$⊢ h = G \to \{h\} = \{G\}$
28	27	fveq2d	$⊢ h = G \to L (\{h\}) = L (\{G\})$
29	28	eqeq2d	$⊢ h = G \to (M (N (\{Y\})) = L (\{h\}) \leftrightarrow M (N (\{Y\})) = L (\{G\}))$
30		oveq2	$⊢ h = G \to F R h = F R G$
31	30	sneqd	$⊢ h = G \to \{F R h\} = \{F R G\}$
32	31	fveq2d	$⊢ h = G \to L (\{F R h\}) = L (\{F R G\})$
33	32	eqeq2d	$⊢ h = G \to (M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}) \leftrightarrow M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\}))$
34	29 33	anbi12d	$⊢ h = G \to ((M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\})) \leftrightarrow (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})))$
35	34	adantl	$⊢ (φ \land h = G) \to ((M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\})) \leftrightarrow (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})))$
36	24 25 26 17 35	riota2df	$⊢ (φ \land \exists! h \in D (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}))) \to ((M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})) \leftrightarrow (ι h \in D \| (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}))) = G)$
37	23 36	mpdan	$⊢ φ \to ((M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})) \leftrightarrow (ι h \in D \| (M (N (\{Y\})) = L (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R h\}))) = G)$
38	22 37	bitr4d	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = L (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = L (\{F R G\})))$

Metamath Proof Explorer

Theorem hdmap1eq

Proof