hdmap14lem11

Description: Part of proof of part 14 in Baer p. 50 line 3. (Contributed by NM, 3-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem8.h	$⊢ H = LHyp (K)$
	hdmap14lem8.u	$⊢ U = DVecH (K) (W)$
	hdmap14lem8.v	$⊢ V = {Base}_{U}$
	hdmap14lem8.q	$⊢ \underset{˙}{+} = +_{U}$
	hdmap14lem8.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmap14lem8.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap14lem8.n	$⊢ N = LSpan (U)$
	hdmap14lem8.r	$⊢ R = Scalar (U)$
	hdmap14lem8.b	$⊢ B = {Base}_{R}$
	hdmap14lem8.c	$⊢ C = LCDual (K) (W)$
	hdmap14lem8.d	$⊢ \underset{˙}{✚} = +_{C}$
	hdmap14lem8.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
	hdmap14lem8.p	$⊢ P = Scalar (C)$
	hdmap14lem8.a	$⊢ A = {Base}_{P}$
	hdmap14lem8.s	$⊢ S = HDMap (K) (W)$
	hdmap14lem8.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap14lem8.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap14lem8.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	hdmap14lem8.f	$⊢ φ \to F \in B$
	hdmap14lem8.g	$⊢ φ \to G \in A$
	hdmap14lem8.i	$⊢ φ \to I \in A$
	hdmap14lem8.xx	$⊢ φ \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
	hdmap14lem8.yy	$⊢ φ \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
Assertion	hdmap14lem11	$⊢ φ \to G = I$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem8.h	$⊢ H = LHyp (K)$
2		hdmap14lem8.u	$⊢ U = DVecH (K) (W)$
3		hdmap14lem8.v	$⊢ V = {Base}_{U}$
4		hdmap14lem8.q	$⊢ \underset{˙}{+} = +_{U}$
5		hdmap14lem8.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
6		hdmap14lem8.o	$⊢ \underset{˙}{0} = 0_{U}$
7		hdmap14lem8.n	$⊢ N = LSpan (U)$
8		hdmap14lem8.r	$⊢ R = Scalar (U)$
9		hdmap14lem8.b	$⊢ B = {Base}_{R}$
10		hdmap14lem8.c	$⊢ C = LCDual (K) (W)$
11		hdmap14lem8.d	$⊢ \underset{˙}{✚} = +_{C}$
12		hdmap14lem8.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
13		hdmap14lem8.p	$⊢ P = Scalar (C)$
14		hdmap14lem8.a	$⊢ A = {Base}_{P}$
15		hdmap14lem8.s	$⊢ S = HDMap (K) (W)$
16		hdmap14lem8.k	$⊢ φ \to (K \in HL \land W \in H)$
17		hdmap14lem8.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		hdmap14lem8.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
19		hdmap14lem8.f	$⊢ φ \to F \in B$
20		hdmap14lem8.g	$⊢ φ \to G \in A$
21		hdmap14lem8.i	$⊢ φ \to I \in A$
22		hdmap14lem8.xx	$⊢ φ \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
23		hdmap14lem8.yy	$⊢ φ \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
24	17	eldifad	$⊢ φ \to X \in V$
25	18	eldifad	$⊢ φ \to Y \in V$
26	1 2 3 7 16 24 25	dvh3dim	$⊢ φ \to \exists z \in V \neg z \in N (\{X, Y\})$
27		eqid	$⊢ LSpan (C) = LSpan (C)$
28	16	3ad2ant1	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to (K \in HL \land W \in H)$
29		simp2	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to z \in V$
30	19	3ad2ant1	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to F \in B$
31	1 2 3 5 8 9 10 12 27 13 14 15 28 29 30	hdmap14lem2a	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to \exists g \in A S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)$
32		simp11	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to φ$
33	32 16	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to (K \in HL \land W \in H)$
34		eqid	$⊢ LSubSp (U) = LSubSp (U)$
35	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
36	32 35	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to U \in LMod$
37	3 34 7 35 24 25	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
38	32 37	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to N (\{X, Y\}) \in LSubSp (U)$
39		simp12	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to z \in V$
40		simp13	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to \neg z \in N (\{X, Y\})$
41	6 34 36 38 39 40	lssneln0	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to z \in (V ∖ \{\underset{˙}{0}\})$
42	32 17	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to X \in (V ∖ \{\underset{˙}{0}\})$
43	32 19	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to F \in B$
44		simp2	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to g \in A$
45	32 20	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to G \in A$
46		simp3	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)$
47	32 22	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
48	1 2 16	dvhlvec	$⊢ φ \to U \in LVec$
49	32 48	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to U \in LVec$
50	32 24	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to X \in V$
51	32 25	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to Y \in V$
52	3 7 49 39 50 51 40	lspindpi	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to (N (\{z\}) \neq N (\{X\}) \land N (\{z\}) \neq N (\{Y\}))$
53	52	simpld	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to N (\{z\}) \neq N (\{X\})$
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 42 43 44 45 46 47 53	hdmap14lem10	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to g = G$
55	32 18	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to Y \in (V ∖ \{\underset{˙}{0}\})$
56	32 21	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to I \in A$
57	32 23	syl	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
58	52	simprd	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to N (\{z\}) \neq N (\{Y\})$
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 55 43 44 56 46 57 58	hdmap14lem10	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to g = I$
60	54 59	eqtr3d	$⊢ ((φ \land z \in V \land \neg z \in N (\{X, Y\})) \land g \in A \land S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z)) \to G = I$
61	60	rexlimdv3a	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to (\exists g \in A S (F \underset{˙}{\cdot} z) = g \underset{˙}{∙} S (z) \to G = I)$
62	31 61	mpd	$⊢ (φ \land z \in V \land \neg z \in N (\{X, Y\})) \to G = I$
63	62	rexlimdv3a	$⊢ φ \to (\exists z \in V \neg z \in N (\{X, Y\}) \to G = I)$
64	26 63	mpd	$⊢ φ \to G = I$

Metamath Proof Explorer

Theorem hdmap14lem11

Proof