mapdpglem32

Description: Lemma for mapdpg . Uniqueness part - consolidate hypotheses in mapdpglem31 . (Contributed by NM, 23-Mar-2015)

	Ref	Expression
Hypotheses	mapdpg.h	$⊢ H = LHyp (K)$
	mapdpg.m	$⊢ M = mapd (K) (W)$
	mapdpg.u	$⊢ U = DVecH (K) (W)$
	mapdpg.v	$⊢ V = {Base}_{U}$
	mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
	mapdpg.n	$⊢ N = LSpan (U)$
	mapdpg.c	$⊢ C = LCDual (K) (W)$
	mapdpg.f	$⊢ F = {Base}_{C}$
	mapdpg.r	$⊢ R = -_{C}$
	mapdpg.j	$⊢ J = LSpan (C)$
	mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdpg.g	$⊢ φ \to G \in F$
	mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
Assertion	mapdpglem32	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to h = i$

Proof

Step	Hyp	Ref	Expression
1		mapdpg.h	$⊢ H = LHyp (K)$
2		mapdpg.m	$⊢ M = mapd (K) (W)$
3		mapdpg.u	$⊢ U = DVecH (K) (W)$
4		mapdpg.v	$⊢ V = {Base}_{U}$
5		mapdpg.s	$⊢ \underset{˙}{-} = -_{U}$
6		mapdpg.z	$⊢ \underset{˙}{0} = 0_{U}$
7		mapdpg.n	$⊢ N = LSpan (U)$
8		mapdpg.c	$⊢ C = LCDual (K) (W)$
9		mapdpg.f	$⊢ F = {Base}_{C}$
10		mapdpg.r	$⊢ R = -_{C}$
11		mapdpg.j	$⊢ J = LSpan (C)$
12		mapdpg.k	$⊢ φ \to (K \in HL \land W \in H)$
13		mapdpg.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
14		mapdpg.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
15		mapdpg.g	$⊢ φ \to G \in F$
16		mapdpg.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
17		mapdpg.e	$⊢ φ \to M (N (\{X\})) = J (\{G\})$
18	12	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (K \in HL \land W \in H)$
19	13	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to X \in (V ∖ \{\underset{˙}{0}\})$
20	14	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to Y \in (V ∖ \{\underset{˙}{0}\})$
21	15	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to G \in F$
22	16	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to N (\{X\}) \neq N (\{Y\})$
23	17	3ad2ant1	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to M (N (\{X\})) = J (\{G\})$
24		simp2l	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to h \in F$
25		simp3l	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
26	24 25	jca	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
27		simp2r	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to i \in F$
28		simp3r	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))$
29	27 28	jca	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
30		eqid	$⊢ Scalar (U) = Scalar (U)$
31		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
32		eqid	$⊢ \cdot_{C} = \cdot_{C}$
33		eqid	$⊢ 0_{Scalar (U)} = 0_{Scalar (U)}$
34	1 2 3 4 5 6 7 8 9 10 11 18 19 20 21 22 23 26 29 30 31 32 33	mapdpglem26	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to \exists u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) h = u \cdot_{C} i$
35	1 2 3 4 5 6 7 8 9 10 11 18 19 20 21 22 23 26 29 30 31 32 33	mapdpglem27	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to \exists v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) G R h = v \cdot_{C} (G R i)$
36		reeanv	$⊢ \exists u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \exists v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i)) \leftrightarrow (\exists u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) h = u \cdot_{C} i \land \exists v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) G R h = v \cdot_{C} (G R i))$
37	34 35 36	sylanbrc	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to \exists u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \exists v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))$
38	18	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to (K \in HL \land W \in H)$
39	19	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to X \in (V ∖ \{\underset{˙}{0}\})$
40	20	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to Y \in (V ∖ \{\underset{˙}{0}\})$
41	21	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to G \in F$
42	22	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to N (\{X\}) \neq N (\{Y\})$
43	23	3ad2ant1	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to M (N (\{X\})) = J (\{G\})$
44		simp12l	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to h \in F$
45		simp13l	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\}))$
46	44 45	jca	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to (h \in F \land (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})))$
47		simp12r	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to i \in F$
48		simp13r	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\}))$
49	47 48	jca	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to (i \in F \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))$
50		eldifi	$⊢ v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \to v \in {Base}_{Scalar (U)}$
51	50	adantl	$⊢ (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \to v \in {Base}_{Scalar (U)}$
52	51	3ad2ant2	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to v \in {Base}_{Scalar (U)}$
53		simp3l	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to h = u \cdot_{C} i$
54		simp3r	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to G R h = v \cdot_{C} (G R i)$
55		eldifi	$⊢ u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \to u \in {Base}_{Scalar (U)}$
56	55	adantr	$⊢ (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \to u \in {Base}_{Scalar (U)}$
57	56	3ad2ant2	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to u \in {Base}_{Scalar (U)}$
58	1 2 3 4 5 6 7 8 9 10 11 38 39 40 41 42 43 46 49 30 31 32 33 52 53 54 57	mapdpglem31	$⊢ ((φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \land (u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \land (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i))) \to h = i$
59	58	3exp	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to ((u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \land v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\})) \to ((h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i)) \to h = i))$
60	59	rexlimdvv	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to (\exists u \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) \exists v \in ({Base}_{Scalar (U)} ∖ \{0_{Scalar (U)}\}) (h = u \cdot_{C} i \land G R h = v \cdot_{C} (G R i)) \to h = i)$
61	37 60	mpd	$⊢ (φ \land (h \in F \land i \in F) \land ((M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R h\})) \land (M (N (\{Y\})) = J (\{i\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{G R i\})))) \to h = i$

Metamath Proof Explorer

Theorem mapdpglem32

Proof