hdmaprnlem16N

Description: Lemma for hdmaprnN . Eliminate v . (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem15.h	$⊢ H = LHyp (K)$
	hdmaprnlem15.u	$⊢ U = DVecH (K) (W)$
	hdmaprnlem15.v	$⊢ V = {Base}_{U}$
	hdmaprnlem15.n	$⊢ N = LSpan (U)$
	hdmaprnlem15.c	$⊢ C = LCDual (K) (W)$
	hdmaprnlem15.d	$⊢ D = {Base}_{C}$
	hdmaprnlem15.q	$⊢ \underset{˙}{0} = 0_{C}$
	hdmaprnlem15.l	$⊢ L = LSpan (C)$
	hdmaprnlem15.m	$⊢ M = mapd (K) (W)$
	hdmaprnlem15.s	$⊢ S = HDMap (K) (W)$
	hdmaprnlem15.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmaprnlem16.se	$⊢ φ \to s \in (D ∖ \{\underset{˙}{0}\})$
Assertion	hdmaprnlem16N	$⊢ φ \to s \in ran S$

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem15.h	$⊢ H = LHyp (K)$
2		hdmaprnlem15.u	$⊢ U = DVecH (K) (W)$
3		hdmaprnlem15.v	$⊢ V = {Base}_{U}$
4		hdmaprnlem15.n	$⊢ N = LSpan (U)$
5		hdmaprnlem15.c	$⊢ C = LCDual (K) (W)$
6		hdmaprnlem15.d	$⊢ D = {Base}_{C}$
7		hdmaprnlem15.q	$⊢ \underset{˙}{0} = 0_{C}$
8		hdmaprnlem15.l	$⊢ L = LSpan (C)$
9		hdmaprnlem15.m	$⊢ M = mapd (K) (W)$
10		hdmaprnlem15.s	$⊢ S = HDMap (K) (W)$
11		hdmaprnlem15.k	$⊢ φ \to (K \in HL \land W \in H)$
12		hdmaprnlem16.se	$⊢ φ \to s \in (D ∖ \{\underset{˙}{0}\})$
13	1 2 11	dvhlmod	$⊢ φ \to U \in LMod$
14		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
15		eqid	$⊢ LSAtoms (C) = LSAtoms (C)$
16	1 5 11	lcdlmod	$⊢ φ \to C \in LMod$
17	6 8 7 15 16 12	lsatlspsn	$⊢ φ \to L (\{s\}) \in LSAtoms (C)$
18	1 9 2 14 5 15 11 17	mapdcnvatN	$⊢ φ \to M^{-1} (L (\{s\})) \in LSAtoms (U)$
19	3 4 14	islsati	$⊢ (U \in LMod \land M^{-1} (L (\{s\})) \in LSAtoms (U)) \to \exists v \in V M^{-1} (L (\{s\})) = N (\{v\})$
20	13 18 19	syl2anc	$⊢ φ \to \exists v \in V M^{-1} (L (\{s\})) = N (\{v\})$
21		simpr	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to M^{-1} (L (\{s\})) = N (\{v\})$
22	21	fveq2d	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to M (M^{-1} (L (\{s\}))) = M (N (\{v\}))$
23	11	ad2antrr	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to (K \in HL \land W \in H)$
24	12	eldifad	$⊢ φ \to s \in D$
25		eqid	$⊢ LSubSp (C) = LSubSp (C)$
26	6 25 8	lspsncl	$⊢ (C \in LMod \land s \in D) \to L (\{s\}) \in LSubSp (C)$
27	16 24 26	syl2anc	$⊢ φ \to L (\{s\}) \in LSubSp (C)$
28	1 9 5 25 11	mapdrn2	$⊢ φ \to ran M = LSubSp (C)$
29	27 28	eleqtrrd	$⊢ φ \to L (\{s\}) \in ran M$
30	29	ad2antrr	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to L (\{s\}) \in ran M$
31	1 9 23 30	mapdcnvid2	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to M (M^{-1} (L (\{s\}))) = L (\{s\})$
32	22 31	eqtr3d	$⊢ ((φ \land v \in V) \land M^{-1} (L (\{s\})) = N (\{v\})) \to M (N (\{v\})) = L (\{s\})$
33	32	ex	$⊢ (φ \land v \in V) \to (M^{-1} (L (\{s\})) = N (\{v\}) \to M (N (\{v\})) = L (\{s\}))$
34	33	reximdva	$⊢ φ \to (\exists v \in V M^{-1} (L (\{s\})) = N (\{v\}) \to \exists v \in V M (N (\{v\})) = L (\{s\}))$
35	20 34	mpd	$⊢ φ \to \exists v \in V M (N (\{v\})) = L (\{s\})$
36	11	3ad2ant1	$⊢ (φ \land v \in V \land M (N (\{v\})) = L (\{s\})) \to (K \in HL \land W \in H)$
37	12	3ad2ant1	$⊢ (φ \land v \in V \land M (N (\{v\})) = L (\{s\})) \to s \in (D ∖ \{\underset{˙}{0}\})$
38		simp2	$⊢ (φ \land v \in V \land M (N (\{v\})) = L (\{s\})) \to v \in V$
39		simp3	$⊢ (φ \land v \in V \land M (N (\{v\})) = L (\{s\})) \to M (N (\{v\})) = L (\{s\})$
40	1 2 3 4 5 6 7 8 9 10 36 37 38 39	hdmaprnlem15N	$⊢ (φ \land v \in V \land M (N (\{v\})) = L (\{s\})) \to s \in ran S$
41	40	rexlimdv3a	$⊢ φ \to (\exists v \in V M (N (\{v\})) = L (\{s\}) \to s \in ran S)$
42	35 41	mpd	$⊢ φ \to s \in ran S$

Metamath Proof Explorer

Theorem hdmaprnlem16N

Proof