hdmap10

Description: Part 10 in Baer p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap10.h	$⊢ H = LHyp (K)$
	hdmap10.u	$⊢ U = DVecH (K) (W)$
	hdmap10.v	$⊢ V = {Base}_{U}$
	hdmap10.n	$⊢ N = LSpan (U)$
	hdmap10.c	$⊢ C = LCDual (K) (W)$
	hdmap10.l	$⊢ L = LSpan (C)$
	hdmap10.m	$⊢ M = mapd (K) (W)$
	hdmap10.s	$⊢ S = HDMap (K) (W)$
	hdmap10.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap10.t	$⊢ φ \to T \in V$
Assertion	hdmap10	$⊢ φ \to M (N (\{T\})) = L (\{S (T)\})$

Proof

Step	Hyp	Ref	Expression
1		hdmap10.h	$⊢ H = LHyp (K)$
2		hdmap10.u	$⊢ U = DVecH (K) (W)$
3		hdmap10.v	$⊢ V = {Base}_{U}$
4		hdmap10.n	$⊢ N = LSpan (U)$
5		hdmap10.c	$⊢ C = LCDual (K) (W)$
6		hdmap10.l	$⊢ L = LSpan (C)$
7		hdmap10.m	$⊢ M = mapd (K) (W)$
8		hdmap10.s	$⊢ S = HDMap (K) (W)$
9		hdmap10.k	$⊢ φ \to (K \in HL \land W \in H)$
10		hdmap10.t	$⊢ φ \to T \in V$
11		sneq	$⊢ T = 0_{U} \to \{T\} = \{0_{U}\}$
12	11	fveq2d	$⊢ T = 0_{U} \to N (\{T\}) = N (\{0_{U}\})$
13	12	fveq2d	$⊢ T = 0_{U} \to M (N (\{T\})) = M (N (\{0_{U}\}))$
14		fveq2	$⊢ T = 0_{U} \to S (T) = S (0_{U})$
15	14	sneqd	$⊢ T = 0_{U} \to \{S (T)\} = \{S (0_{U})\}$
16	15	fveq2d	$⊢ T = 0_{U} \to L (\{S (T)\}) = L (\{S (0_{U})\})$
17	13 16	eqeq12d	$⊢ T = 0_{U} \to (M (N (\{T\})) = L (\{S (T)\}) \leftrightarrow M (N (\{0_{U}\})) = L (\{S (0_{U})\}))$
18	9	adantr	$⊢ (φ \land T \neq 0_{U}) \to (K \in HL \land W \in H)$
19		eqid	$⊢ ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
20		eqid	$⊢ 0_{U} = 0_{U}$
21		eqid	$⊢ {Base}_{C} = {Base}_{C}$
22		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
23		eqid	$⊢ HDMap1 (K) (W) = HDMap1 (K) (W)$
24	10	anim1i	$⊢ (φ \land T \neq 0_{U}) \to (T \in V \land T \neq 0_{U})$
25		eldifsn	$⊢ T \in (V ∖ \{0_{U}\}) \leftrightarrow (T \in V \land T \neq 0_{U})$
26	24 25	sylibr	$⊢ (φ \land T \neq 0_{U}) \to T \in (V ∖ \{0_{U}\})$
27	1 2 3 4 5 6 7 8 18 19 20 21 22 23 26	hdmap10lem	$⊢ (φ \land T \neq 0_{U}) \to M (N (\{T\})) = L (\{S (T)\})$
28	1 2 9	dvhlmod	$⊢ φ \to U \in LMod$
29	20 4	lspsn0	$⊢ U \in LMod \to N (\{0_{U}\}) = \{0_{U}\}$
30	28 29	syl	$⊢ φ \to N (\{0_{U}\}) = \{0_{U}\}$
31	30	fveq2d	$⊢ φ \to M (N (\{0_{U}\})) = M (\{0_{U}\})$
32		eqid	$⊢ 0_{C} = 0_{C}$
33	1 7 2 20 5 32 9	mapd0	$⊢ φ \to M (\{0_{U}\}) = \{0_{C}\}$
34	1 2 20 5 32 8 9	hdmapval0	$⊢ φ \to S (0_{U}) = 0_{C}$
35	34	sneqd	$⊢ φ \to \{S (0_{U})\} = \{0_{C}\}$
36	35	fveq2d	$⊢ φ \to L (\{S (0_{U})\}) = L (\{0_{C}\})$
37	1 5 9	lcdlmod	$⊢ φ \to C \in LMod$
38	32 6	lspsn0	$⊢ C \in LMod \to L (\{0_{C}\}) = \{0_{C}\}$
39	37 38	syl	$⊢ φ \to L (\{0_{C}\}) = \{0_{C}\}$
40	36 39	eqtr2d	$⊢ φ \to \{0_{C}\} = L (\{S (0_{U})\})$
41	31 33 40	3eqtrd	$⊢ φ \to M (N (\{0_{U}\})) = L (\{S (0_{U})\})$
42	17 27 41	pm2.61ne	$⊢ φ \to M (N (\{T\})) = L (\{S (T)\})$

Metamath Proof Explorer

Theorem hdmap10

Proof