hdmap14lem10

Description: Part of proof of part 14 in Baer p. 49 line 38. (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)$
	hdmap14lem8.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
Assertion	hdmap14lem10	$⊢ φ \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		hdmap14lem8.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
25		eqid	$⊢ LSpan (C) = LSpan (C)$
26	1 2 16	dvhlmod	$⊢ φ \to U \in LMod$
27	17	eldifad	$⊢ φ \to X \in V$
28	18	eldifad	$⊢ φ \to Y \in V$
29	3 4	lmodvacl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
30	26 27 28 29	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in V$
31	1 2 3 5 8 9 10 12 25 13 14 15 16 30 19	hdmap14lem2a	$⊢ φ \to \exists g \in A S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)$
32	16	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to (K \in HL \land W \in H)$
33	17	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to X \in (V ∖ \{\underset{˙}{0}\})$
34	18	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to Y \in (V ∖ \{\underset{˙}{0}\})$
35	19	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to F \in B$
36	20	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to G \in A$
37	21	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to I \in A$
38	22	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
39	23	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to S (F \underset{˙}{\cdot} Y) = I \underset{˙}{∙} S (Y)$
40	24	3ad2ant1	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to N (\{X\}) \neq N (\{Y\})$
41		simp2	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to g \in A$
42		simp3	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)$
43	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41 42	hdmap14lem9	$⊢ (φ \land g \in A \land S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y)) \to G = I$
44	43	rexlimdv3a	$⊢ φ \to (\exists g \in A S (F \underset{˙}{\cdot} (X \underset{˙}{+} Y)) = g \underset{˙}{∙} S (X \underset{˙}{+} Y) \to G = I)$
45	31 44	mpd	$⊢ φ \to G = I$

Metamath Proof Explorer

Theorem hdmap14lem10

Proof