eqlkr3

Description: Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015)

	Ref	Expression
Hypotheses	eqlkr3.v	$⊢ V = {Base}_{W}$
	eqlkr3.s	$⊢ S = Scalar (W)$
	eqlkr3.r	$⊢ R = {Base}_{S}$
	eqlkr3.o	$⊢ \underset{˙}{0} = 0_{S}$
	eqlkr3.f	$⊢ F = LFnl (W)$
	eqlkr3.k	$⊢ K = LKer (W)$
	eqlkr3.w	$⊢ φ \to W \in LVec$
	eqlkr3.x	$⊢ φ \to X \in V$
	eqlkr3.g	$⊢ φ \to G \in F$
	eqlkr3.h	$⊢ φ \to H \in F$
	eqlkr3.e	$⊢ φ \to K (G) = K (H)$
	eqlkr3.a	$⊢ φ \to G (X) = H (X)$
	eqlkr3.n	$⊢ φ \to G (X) \neq \underset{˙}{0}$
Assertion	eqlkr3	$⊢ φ \to G = H$

Proof

Step	Hyp	Ref	Expression
1		eqlkr3.v	$⊢ V = {Base}_{W}$
2		eqlkr3.s	$⊢ S = Scalar (W)$
3		eqlkr3.r	$⊢ R = {Base}_{S}$
4		eqlkr3.o	$⊢ \underset{˙}{0} = 0_{S}$
5		eqlkr3.f	$⊢ F = LFnl (W)$
6		eqlkr3.k	$⊢ K = LKer (W)$
7		eqlkr3.w	$⊢ φ \to W \in LVec$
8		eqlkr3.x	$⊢ φ \to X \in V$
9		eqlkr3.g	$⊢ φ \to G \in F$
10		eqlkr3.h	$⊢ φ \to H \in F$
11		eqlkr3.e	$⊢ φ \to K (G) = K (H)$
12		eqlkr3.a	$⊢ φ \to G (X) = H (X)$
13		eqlkr3.n	$⊢ φ \to G (X) \neq \underset{˙}{0}$
14	2 3 1 5	lflf	$⊢ (W \in LVec \land G \in F) \to G : V ⟶ R$
15	7 9 14	syl2anc	$⊢ φ \to G : V ⟶ R$
16	15	ffnd	$⊢ φ \to G Fn V$
17	2 3 1 5	lflf	$⊢ (W \in LVec \land H \in F) \to H : V ⟶ R$
18	7 10 17	syl2anc	$⊢ φ \to H : V ⟶ R$
19	18	ffnd	$⊢ φ \to H Fn V$
20		eqid	$⊢ \cdot_{S} = \cdot_{S}$
21	2 3 20 1 5 6	eqlkr	$⊢ (W \in LVec \land (G \in F \land H \in F) \land K (G) = K (H)) \to \exists r \in R \forall x \in V H (x) = G (x) \cdot_{S} r$
22	7 9 10 11 21	syl121anc	$⊢ φ \to \exists r \in R \forall x \in V H (x) = G (x) \cdot_{S} r$
23	8	adantr	$⊢ (φ \land r \in R) \to X \in V$
24		fveq2	$⊢ x = X \to H (x) = H (X)$
25		fveq2	$⊢ x = X \to G (x) = G (X)$
26	25	oveq1d	$⊢ x = X \to G (x) \cdot_{S} r = G (X) \cdot_{S} r$
27	24 26	eqeq12d	$⊢ x = X \to (H (x) = G (x) \cdot_{S} r \leftrightarrow H (X) = G (X) \cdot_{S} r)$
28	27	rspcv	$⊢ X \in V \to (\forall x \in V H (x) = G (x) \cdot_{S} r \to H (X) = G (X) \cdot_{S} r)$
29	23 28	syl	$⊢ (φ \land r \in R) \to (\forall x \in V H (x) = G (x) \cdot_{S} r \to H (X) = G (X) \cdot_{S} r)$
30	12	adantr	$⊢ (φ \land r \in R) \to G (X) = H (X)$
31	30	adantr	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to G (X) = H (X)$
32		simpr	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to H (X) = G (X) \cdot_{S} r$
33	31 32	eqtr2d	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to G (X) \cdot_{S} r = G (X)$
34	33	oveq2d	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to {inv}_{r} (S) (G (X)) \cdot_{S} (G (X) \cdot_{S} r) = {inv}_{r} (S) (G (X)) \cdot_{S} G (X)$
35	2	lvecdrng	$⊢ W \in LVec \to S \in DivRing$
36	7 35	syl	$⊢ φ \to S \in DivRing$
37	36	adantr	$⊢ (φ \land r \in R) \to S \in DivRing$
38	2 3 1 5	lflcl	$⊢ (W \in LVec \land G \in F \land X \in V) \to G (X) \in R$
39	7 9 8 38	syl3anc	$⊢ φ \to G (X) \in R$
40	39	adantr	$⊢ (φ \land r \in R) \to G (X) \in R$
41	13	adantr	$⊢ (φ \land r \in R) \to G (X) \neq \underset{˙}{0}$
42		eqid	$⊢ 1_{S} = 1_{S}$
43		eqid	$⊢ {inv}_{r} (S) = {inv}_{r} (S)$
44	3 4 20 42 43	drnginvrl	$⊢ (S \in DivRing \land G (X) \in R \land G (X) \neq \underset{˙}{0}) \to {inv}_{r} (S) (G (X)) \cdot_{S} G (X) = 1_{S}$
45	37 40 41 44	syl3anc	$⊢ (φ \land r \in R) \to {inv}_{r} (S) (G (X)) \cdot_{S} G (X) = 1_{S}$
46	45	oveq1d	$⊢ (φ \land r \in R) \to ({inv}_{r} (S) (G (X)) \cdot_{S} G (X)) \cdot_{S} r = 1_{S} \cdot_{S} r$
47		lveclmod	$⊢ W \in LVec \to W \in LMod$
48	7 47	syl	$⊢ φ \to W \in LMod$
49	2	lmodring	$⊢ W \in LMod \to S \in Ring$
50	48 49	syl	$⊢ φ \to S \in Ring$
51	50	adantr	$⊢ (φ \land r \in R) \to S \in Ring$
52	3 4 43	drnginvrcl	$⊢ (S \in DivRing \land G (X) \in R \land G (X) \neq \underset{˙}{0}) \to {inv}_{r} (S) (G (X)) \in R$
53	37 40 41 52	syl3anc	$⊢ (φ \land r \in R) \to {inv}_{r} (S) (G (X)) \in R$
54		simpr	$⊢ (φ \land r \in R) \to r \in R$
55	3 20	ringass	$⊢ (S \in Ring \land ({inv}_{r} (S) (G (X)) \in R \land G (X) \in R \land r \in R)) \to ({inv}_{r} (S) (G (X)) \cdot_{S} G (X)) \cdot_{S} r = {inv}_{r} (S) (G (X)) \cdot_{S} (G (X) \cdot_{S} r)$
56	51 53 40 54 55	syl13anc	$⊢ (φ \land r \in R) \to ({inv}_{r} (S) (G (X)) \cdot_{S} G (X)) \cdot_{S} r = {inv}_{r} (S) (G (X)) \cdot_{S} (G (X) \cdot_{S} r)$
57	3 20 42	ringlidm	$⊢ (S \in Ring \land r \in R) \to 1_{S} \cdot_{S} r = r$
58	51 54 57	syl2anc	$⊢ (φ \land r \in R) \to 1_{S} \cdot_{S} r = r$
59	46 56 58	3eqtr3d	$⊢ (φ \land r \in R) \to {inv}_{r} (S) (G (X)) \cdot_{S} (G (X) \cdot_{S} r) = r$
60	59	adantr	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to {inv}_{r} (S) (G (X)) \cdot_{S} (G (X) \cdot_{S} r) = r$
61	45	adantr	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to {inv}_{r} (S) (G (X)) \cdot_{S} G (X) = 1_{S}$
62	34 60 61	3eqtr3d	$⊢ ((φ \land r \in R) \land H (X) = G (X) \cdot_{S} r) \to r = 1_{S}$
63	62	ex	$⊢ (φ \land r \in R) \to (H (X) = G (X) \cdot_{S} r \to r = 1_{S})$
64	29 63	syld	$⊢ (φ \land r \in R) \to (\forall x \in V H (x) = G (x) \cdot_{S} r \to r = 1_{S})$
65	64	ancrd	$⊢ (φ \land r \in R) \to (\forall x \in V H (x) = G (x) \cdot_{S} r \to (r = 1_{S} \land \forall x \in V H (x) = G (x) \cdot_{S} r))$
66	65	reximdva	$⊢ φ \to (\exists r \in R \forall x \in V H (x) = G (x) \cdot_{S} r \to \exists r \in R (r = 1_{S} \land \forall x \in V H (x) = G (x) \cdot_{S} r))$
67	22 66	mpd	$⊢ φ \to \exists r \in R (r = 1_{S} \land \forall x \in V H (x) = G (x) \cdot_{S} r)$
68	3 42	ringidcl	$⊢ S \in Ring \to 1_{S} \in R$
69	50 68	syl	$⊢ φ \to 1_{S} \in R$
70		oveq2	$⊢ r = 1_{S} \to G (x) \cdot_{S} r = G (x) \cdot_{S} 1_{S}$
71	70	eqeq2d	$⊢ r = 1_{S} \to (H (x) = G (x) \cdot_{S} r \leftrightarrow H (x) = G (x) \cdot_{S} 1_{S})$
72	71	ralbidv	$⊢ r = 1_{S} \to (\forall x \in V H (x) = G (x) \cdot_{S} r \leftrightarrow \forall x \in V H (x) = G (x) \cdot_{S} 1_{S})$
73	72	ceqsrexv	$⊢ 1_{S} \in R \to (\exists r \in R (r = 1_{S} \land \forall x \in V H (x) = G (x) \cdot_{S} r) \leftrightarrow \forall x \in V H (x) = G (x) \cdot_{S} 1_{S})$
74	69 73	syl	$⊢ φ \to (\exists r \in R (r = 1_{S} \land \forall x \in V H (x) = G (x) \cdot_{S} r) \leftrightarrow \forall x \in V H (x) = G (x) \cdot_{S} 1_{S})$
75	67 74	mpbid	$⊢ φ \to \forall x \in V H (x) = G (x) \cdot_{S} 1_{S}$
76	75	r19.21bi	$⊢ (φ \land x \in V) \to H (x) = G (x) \cdot_{S} 1_{S}$
77	48	adantr	$⊢ (φ \land x \in V) \to W \in LMod$
78	77 49	syl	$⊢ (φ \land x \in V) \to S \in Ring$
79	7	adantr	$⊢ (φ \land x \in V) \to W \in LVec$
80	9	adantr	$⊢ (φ \land x \in V) \to G \in F$
81		simpr	$⊢ (φ \land x \in V) \to x \in V$
82	2 3 1 5	lflcl	$⊢ (W \in LVec \land G \in F \land x \in V) \to G (x) \in R$
83	79 80 81 82	syl3anc	$⊢ (φ \land x \in V) \to G (x) \in R$
84	3 20 42	ringridm	$⊢ (S \in Ring \land G (x) \in R) \to G (x) \cdot_{S} 1_{S} = G (x)$
85	78 83 84	syl2anc	$⊢ (φ \land x \in V) \to G (x) \cdot_{S} 1_{S} = G (x)$
86	76 85	eqtr2d	$⊢ (φ \land x \in V) \to G (x) = H (x)$
87	16 19 86	eqfnfvd	$⊢ φ \to G = H$

Metamath Proof Explorer

Theorem eqlkr3

Proof