eqlkr2

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014)

	Ref	Expression
Hypotheses	eqlkr.d	$⊢ D = Scalar (W)$
	eqlkr.k	$⊢ K = {Base}_{D}$
	eqlkr.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	eqlkr.v	$⊢ V = {Base}_{W}$
	eqlkr.f	$⊢ F = LFnl (W)$
	eqlkr.l	$⊢ L = LKer (W)$
Assertion	eqlkr2	$⊢ (W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \to \exists r \in K H = G {\underset{˙}{\cdot}}_{f} (V \times \{r\})$

Proof

Step	Hyp	Ref	Expression
1		eqlkr.d	$⊢ D = Scalar (W)$
2		eqlkr.k	$⊢ K = {Base}_{D}$
3		eqlkr.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
4		eqlkr.v	$⊢ V = {Base}_{W}$
5		eqlkr.f	$⊢ F = LFnl (W)$
6		eqlkr.l	$⊢ L = LKer (W)$
7	1 2 3 4 5 6	eqlkr	$⊢ (W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
8	4	fvexi	$⊢ V \in V$
9	8	a1i	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to V \in V$
10		simpl1	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to W \in LVec$
11		simpl2l	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to G \in F$
12	1 2 4 5	lflf	$⊢ (W \in LVec \land G \in F) \to G : V ⟶ K$
13	10 11 12	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to G : V ⟶ K$
14	13	ffnd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to G Fn V$
15		vex	$⊢ r \in V$
16		fnconstg	$⊢ r \in V \to (V \times \{r\}) Fn V$
17	15 16	mp1i	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to (V \times \{r\}) Fn V$
18		simpl2r	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to H \in F$
19	1 2 4 5	lflf	$⊢ (W \in LVec \land H \in F) \to H : V ⟶ K$
20	10 18 19	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to H : V ⟶ K$
21	20	ffnd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to H Fn V$
22		eqidd	$⊢ (((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \land x \in V) \to G (x) = G (x)$
23	15	fvconst2	$⊢ x \in V \to (V \times \{r\}) (x) = r$
24	23	adantl	$⊢ (((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \land x \in V) \to (V \times \{r\}) (x) = r$
25	9 14 17 21 22 24	offveqb	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land r \in K) \to (H = G {\underset{˙}{\cdot}}_{f} (V \times \{r\}) \leftrightarrow \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r)$
26	25	rexbidva	$⊢ (W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \to (\exists r \in K H = G {\underset{˙}{\cdot}}_{f} (V \times \{r\}) \leftrightarrow \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r)$
27	7 26	mpbird	$⊢ (W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \to \exists r \in K H = G {\underset{˙}{\cdot}}_{f} (V \times \{r\})$

Metamath Proof Explorer

Theorem eqlkr2

Proof