hdmap14lem14

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

	Ref	Expression
Hypotheses	hdmap14lem12.h	$⊢ H = LHyp (K)$
	hdmap14lem12.u	$⊢ U = DVecH (K) (W)$
	hdmap14lem12.v	$⊢ V = {Base}_{U}$
	hdmap14lem12.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmap14lem12.r	$⊢ R = Scalar (U)$
	hdmap14lem12.b	$⊢ B = {Base}_{R}$
	hdmap14lem12.c	$⊢ C = LCDual (K) (W)$
	hdmap14lem12.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
	hdmap14lem12.s	$⊢ S = HDMap (K) (W)$
	hdmap14lem12.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap14lem12.f	$⊢ φ \to F \in B$
	hdmap14lem12.p	$⊢ P = Scalar (C)$
	hdmap14lem12.a	$⊢ A = {Base}_{P}$
Assertion	hdmap14lem14	$⊢ φ \to \exists! g \in A \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x)$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	$⊢ H = LHyp (K)$
2		hdmap14lem12.u	$⊢ U = DVecH (K) (W)$
3		hdmap14lem12.v	$⊢ V = {Base}_{U}$
4		hdmap14lem12.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
5		hdmap14lem12.r	$⊢ R = Scalar (U)$
6		hdmap14lem12.b	$⊢ B = {Base}_{R}$
7		hdmap14lem12.c	$⊢ C = LCDual (K) (W)$
8		hdmap14lem12.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
9		hdmap14lem12.s	$⊢ S = HDMap (K) (W)$
10		hdmap14lem12.k	$⊢ φ \to (K \in HL \land W \in H)$
11		hdmap14lem12.f	$⊢ φ \to F \in B$
12		hdmap14lem12.p	$⊢ P = Scalar (C)$
13		hdmap14lem12.a	$⊢ A = {Base}_{P}$
14		eqid	$⊢ 0_{U} = 0_{U}$
15	1 2 3 14 10	dvh1dim	$⊢ φ \to \exists y \in V y \neq 0_{U}$
16	10	3ad2ant1	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to (K \in HL \land W \in H)$
17		3simpc	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to (y \in V \land y \neq 0_{U})$
18		eldifsn	$⊢ y \in (V ∖ \{0_{U}\}) \leftrightarrow (y \in V \land y \neq 0_{U})$
19	17 18	sylibr	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to y \in (V ∖ \{0_{U}\})$
20	11	3ad2ant1	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to F \in B$
21	1 2 3 4 14 5 6 7 8 12 13 9 16 19 20	hdmap14lem7	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to \exists! g \in A S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)$
22		simpl1	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to φ$
23	22 10	syl	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to (K \in HL \land W \in H)$
24	22 11	syl	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to F \in B$
25	19	adantr	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to y \in (V ∖ \{0_{U}\})$
26		simpr	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to g \in A$
27	1 2 3 4 5 6 7 8 9 23 24 12 13 14 25 26	hdmap14lem13	$⊢ ((φ \land y \in V \land y \neq 0_{U}) \land g \in A) \to (S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y) \leftrightarrow \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x))$
28	27	reubidva	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to (\exists! g \in A S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y) \leftrightarrow \exists! g \in A \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x))$
29	21 28	mpbid	$⊢ (φ \land y \in V \land y \neq 0_{U}) \to \exists! g \in A \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x)$
30	29	rexlimdv3a	$⊢ φ \to (\exists y \in V y \neq 0_{U} \to \exists! g \in A \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x))$
31	15 30	mpd	$⊢ φ \to \exists! g \in A \forall x \in V S (F \underset{˙}{\cdot} x) = g \underset{˙}{∙} S (x)$

Metamath Proof Explorer

Theorem hdmap14lem14

Proof