hgmaprnlem4N

Description: Lemma for hgmaprnN . Eliminate s . (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmaprnlem1.h	$⊢ H = LHyp (K)$
	hgmaprnlem1.u	$⊢ U = DVecH (K) (W)$
	hgmaprnlem1.v	$⊢ V = {Base}_{U}$
	hgmaprnlem1.r	$⊢ R = Scalar (U)$
	hgmaprnlem1.b	$⊢ B = {Base}_{R}$
	hgmaprnlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hgmaprnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
	hgmaprnlem1.c	$⊢ C = LCDual (K) (W)$
	hgmaprnlem1.d	$⊢ D = {Base}_{C}$
	hgmaprnlem1.p	$⊢ P = Scalar (C)$
	hgmaprnlem1.a	$⊢ A = {Base}_{P}$
	hgmaprnlem1.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
	hgmaprnlem1.q	$⊢ Q = 0_{C}$
	hgmaprnlem1.s	$⊢ S = HDMap (K) (W)$
	hgmaprnlem1.g	$⊢ G = HGMap (K) (W)$
	hgmaprnlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	hgmaprnlem1.z	$⊢ φ \to z \in A$
	hgmaprnlem1.t2	$⊢ φ \to t \in (V ∖ \{\underset{˙}{0}\})$
Assertion	hgmaprnlem4N	$⊢ φ \to z \in ran G$

Proof

Step	Hyp	Ref	Expression
1		hgmaprnlem1.h	$⊢ H = LHyp (K)$
2		hgmaprnlem1.u	$⊢ U = DVecH (K) (W)$
3		hgmaprnlem1.v	$⊢ V = {Base}_{U}$
4		hgmaprnlem1.r	$⊢ R = Scalar (U)$
5		hgmaprnlem1.b	$⊢ B = {Base}_{R}$
6		hgmaprnlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		hgmaprnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
8		hgmaprnlem1.c	$⊢ C = LCDual (K) (W)$
9		hgmaprnlem1.d	$⊢ D = {Base}_{C}$
10		hgmaprnlem1.p	$⊢ P = Scalar (C)$
11		hgmaprnlem1.a	$⊢ A = {Base}_{P}$
12		hgmaprnlem1.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
13		hgmaprnlem1.q	$⊢ Q = 0_{C}$
14		hgmaprnlem1.s	$⊢ S = HDMap (K) (W)$
15		hgmaprnlem1.g	$⊢ G = HGMap (K) (W)$
16		hgmaprnlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
17		hgmaprnlem1.z	$⊢ φ \to z \in A$
18		hgmaprnlem1.t2	$⊢ φ \to t \in (V ∖ \{\underset{˙}{0}\})$
19	1 8 16	lcdlmod	$⊢ φ \to C \in LMod$
20	18	eldifad	$⊢ φ \to t \in V$
21	1 2 3 8 9 14 16 20	hdmapcl	$⊢ φ \to S (t) \in D$
22	9 10 12 11	lmodvscl	$⊢ (C \in LMod \land z \in A \land S (t) \in D) \to z \underset{˙}{∙} S (t) \in D$
23	19 17 21 22	syl3anc	$⊢ φ \to z \underset{˙}{∙} S (t) \in D$
24	1 8 9 14 16	hdmaprnN	$⊢ φ \to ran S = D$
25	23 24	eleqtrrd	$⊢ φ \to z \underset{˙}{∙} S (t) \in ran S$
26	1 2 3 14 16	hdmapfnN	$⊢ φ \to S Fn V$
27		fvelrnb	$⊢ S Fn V \to (z \underset{˙}{∙} S (t) \in ran S \leftrightarrow \exists s \in V S (s) = z \underset{˙}{∙} S (t))$
28	26 27	syl	$⊢ φ \to (z \underset{˙}{∙} S (t) \in ran S \leftrightarrow \exists s \in V S (s) = z \underset{˙}{∙} S (t))$
29	25 28	mpbid	$⊢ φ \to \exists s \in V S (s) = z \underset{˙}{∙} S (t)$
30	16	3ad2ant1	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to (K \in HL \land W \in H)$
31	17	3ad2ant1	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to z \in A$
32	18	3ad2ant1	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to t \in (V ∖ \{\underset{˙}{0}\})$
33		simp2	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to s \in V$
34		simp3	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to S (s) = z \underset{˙}{∙} S (t)$
35		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
36		eqid	$⊢ LSpan (U) = LSpan (U)$
37		eqid	$⊢ LSpan (C) = LSpan (C)$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 30 31 32 33 34 35 36 37	hgmaprnlem3N	$⊢ (φ \land s \in V \land S (s) = z \underset{˙}{∙} S (t)) \to z \in ran G$
39	38	rexlimdv3a	$⊢ φ \to (\exists s \in V S (s) = z \underset{˙}{∙} S (t) \to z \in ran G)$
40	29 39	mpd	$⊢ φ \to z \in ran G$

Metamath Proof Explorer

Theorem hgmaprnlem4N

Proof