mapdh75fN

Description: Part (7) of Baer p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh75.h	$⊢ H = LHyp (K)$
	mapdh75.u	$⊢ U = DVecH (K) (W)$
	mapdh75.v	$⊢ V = {Base}_{U}$
	mapdh75.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdh75.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh75.n	$⊢ N = LSpan (U)$
	mapdh75.c	$⊢ C = LCDual (K) (W)$
	mapdh75.d	$⊢ D = {Base}_{C}$
	mapdh75.r	$⊢ R = -_{C}$
	mapdh75.q	$⊢ Q = 0_{C}$
	mapdh75.j	$⊢ J = LSpan (C)$
	mapdh75.m	$⊢ M = mapd (K) (W)$
	mapdh75.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh75.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdh75.f	$⊢ φ \to F \in D$
	mapdh75.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdh75a	$⊢ φ \to I (⟨X, F, Y⟩) = G$
	mapdh75d.b	$⊢ φ \to I (⟨X, F, Z⟩) = E$
	mapdh75d.vw	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	mapdh75d.un	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	mapdh75d.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdh75d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdh75d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
Assertion	mapdh75fN	$⊢ φ \to I (⟨Z, E, Y⟩) = G$

Proof

Step	Hyp	Ref	Expression
1		mapdh75.h	$⊢ H = LHyp (K)$
2		mapdh75.u	$⊢ U = DVecH (K) (W)$
3		mapdh75.v	$⊢ V = {Base}_{U}$
4		mapdh75.s	$⊢ \underset{˙}{-} = -_{U}$
5		mapdh75.o	$⊢ \underset{˙}{0} = 0_{U}$
6		mapdh75.n	$⊢ N = LSpan (U)$
7		mapdh75.c	$⊢ C = LCDual (K) (W)$
8		mapdh75.d	$⊢ D = {Base}_{C}$
9		mapdh75.r	$⊢ R = -_{C}$
10		mapdh75.q	$⊢ Q = 0_{C}$
11		mapdh75.j	$⊢ J = LSpan (C)$
12		mapdh75.m	$⊢ M = mapd (K) (W)$
13		mapdh75.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
14		mapdh75.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdh75.f	$⊢ φ \to F \in D$
16		mapdh75.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdh75a	$⊢ φ \to I (⟨X, F, Y⟩) = G$
18		mapdh75d.b	$⊢ φ \to I (⟨X, F, Z⟩) = E$
19		mapdh75d.vw	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
20		mapdh75d.un	$⊢ φ \to \neg X \in N (\{Y, Z\})$
21		mapdh75d.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
22		mapdh75d.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
23		mapdh75d.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
24	22	eldifad	$⊢ φ \to Y \in V$
25	1 2 14	dvhlvec	$⊢ φ \to U \in LVec$
26	21	eldifad	$⊢ φ \to X \in V$
27	23	eldifad	$⊢ φ \to Z \in V$
28	3 6 25 26 24 27 20	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
29	28	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
30	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 21 24 29	mapdhcl	$⊢ φ \to I (⟨X, F, Y⟩) \in D$
31	17 30	eqeltrrd	$⊢ φ \to G \in D$
32	10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 21 22 31 29	mapdheq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})))$
33	17 32	mpbid	$⊢ φ \to (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))$
34	33	simpld	$⊢ φ \to M (N (\{Y\})) = J (\{G\})$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	mapdh75d	$⊢ φ \to I (⟨Y, G, Z⟩) = E$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 31 34 35 19 22 23	mapdh75e	$⊢ φ \to I (⟨Z, E, Y⟩) = G$

Metamath Proof Explorer

Theorem mapdh75fN

Proof