eqlkr4

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	eqlkr4.s	$⊢ S = Scalar (W)$
	eqlkr4.r	$⊢ R = {Base}_{S}$
	eqlkr4.f	$⊢ F = LFnl (W)$
	eqlkr4.k	$⊢ K = LKer (W)$
	eqlkr4.d	$⊢ D = LDual (W)$
	eqlkr4.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	eqlkr4.w	$⊢ φ \to W \in LVec$
	eqlkr4.g	$⊢ φ \to G \in F$
	eqlkr4.h	$⊢ φ \to H \in F$
	eqlkr4.e	$⊢ φ \to K (G) = K (H)$
Assertion	eqlkr4	$⊢ φ \to \exists r \in R H = r \underset{˙}{\cdot} G$

Step	Hyp	Ref	Expression
1		eqlkr4.s	$⊢ S = Scalar (W)$
2		eqlkr4.r	$⊢ R = {Base}_{S}$
3		eqlkr4.f	$⊢ F = LFnl (W)$
4		eqlkr4.k	$⊢ K = LKer (W)$
5		eqlkr4.d	$⊢ D = LDual (W)$
6		eqlkr4.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
7		eqlkr4.w	$⊢ φ \to W \in LVec$
8		eqlkr4.g	$⊢ φ \to G \in F$
9		eqlkr4.h	$⊢ φ \to H \in F$
10		eqlkr4.e	$⊢ φ \to K (G) = K (H)$
11		eqid	$⊢ \cdot_{S} = \cdot_{S}$
12		eqid	$⊢ {Base}_{W} = {Base}_{W}$
13	1 2 11 12 3 4	eqlkr2	$⊢ (W \in LVec \land (G \in F \land H \in F) \land K (G) = K (H)) \to \exists r \in R H = G {\cdot_{S}}_{f} ({Base}_{W} \times \{r\})$
14	7 8 9 10 13	syl121anc	$⊢ φ \to \exists r \in R H = G {\cdot_{S}}_{f} ({Base}_{W} \times \{r\})$
15	7	adantr	$⊢ (φ \land r \in R) \to W \in LVec$
16		simpr	$⊢ (φ \land r \in R) \to r \in R$
17	8	adantr	$⊢ (φ \land r \in R) \to G \in F$
18	3 12 1 2 11 5 6 15 16 17	ldualvs	$⊢ (φ \land r \in R) \to r \underset{˙}{\cdot} G = G {\cdot_{S}}_{f} ({Base}_{W} \times \{r\})$
19	18	eqeq2d	$⊢ (φ \land r \in R) \to (H = r \underset{˙}{\cdot} G \leftrightarrow H = G {\cdot_{S}}_{f} ({Base}_{W} \times \{r\}))$
20	19	rexbidva	$⊢ φ \to (\exists r \in R H = r \underset{˙}{\cdot} G \leftrightarrow \exists r \in R H = G {\cdot_{S}}_{f} ({Base}_{W} \times \{r\}))$
21	14 20	mpbird	$⊢ φ \to \exists r \in R H = r \underset{˙}{\cdot} G$

Metamath Proof Explorer