eqlkr

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-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	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$

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		simpl1	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to W \in LVec$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	1	lmodring	$⊢ W \in LMod \to D \in Ring$
10	8 9	syl	$⊢ W \in LVec \to D \in Ring$
11	7 10	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to D \in Ring$
12		eqid	$⊢ 1_{D} = 1_{D}$
13	2 12	ringidcl	$⊢ D \in Ring \to 1_{D} \in K$
14	11 13	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to 1_{D} \in K$
15		simp11	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to W \in LVec$
16	15 10	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to D \in Ring$
17		simp12l	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G \in F$
18		simp3	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to x \in V$
19	1 2 4 5	lflcl	$⊢ (W \in LVec \land G \in F \land x \in V) \to G (x) \in K$
20	15 17 18 19	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G (x) \in K$
21	2 3 12	ringridm	$⊢ (D \in Ring \land G (x) \in K) \to G (x) \underset{˙}{\cdot} 1_{D} = G (x)$
22	16 20 21	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G (x) \underset{˙}{\cdot} 1_{D} = G (x)$
23		simp2	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G = V \times \{0_{D}\}$
24		simp13	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to L (G) = L (H)$
25	15 8	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to W \in LMod$
26		eqid	$⊢ 0_{D} = 0_{D}$
27	1 26 4 5 6	lkr0f	$⊢ (W \in LMod \land G \in F) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
28	25 17 27	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to (L (G) = V \leftrightarrow G = V \times \{0_{D}\})$
29	23 28	mpbird	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to L (G) = V$
30	24 29	eqtr3d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to L (H) = V$
31		simp12r	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to H \in F$
32	1 26 4 5 6	lkr0f	$⊢ (W \in LMod \land H \in F) \to (L (H) = V \leftrightarrow H = V \times \{0_{D}\})$
33	25 31 32	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to (L (H) = V \leftrightarrow H = V \times \{0_{D}\})$
34	30 33	mpbid	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to H = V \times \{0_{D}\}$
35	23 34	eqtr4d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G = H$
36	35	fveq1d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to G (x) = H (x)$
37	22 36	eqtr2d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\} \land x \in V) \to H (x) = G (x) \underset{˙}{\cdot} 1_{D}$
38	37	3expia	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to (x \in V \to H (x) = G (x) \underset{˙}{\cdot} 1_{D})$
39	38	ralrimiv	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to \forall x \in V H (x) = G (x) \underset{˙}{\cdot} 1_{D}$
40		oveq2	$⊢ r = 1_{D} \to G (x) \underset{˙}{\cdot} r = G (x) \underset{˙}{\cdot} 1_{D}$
41	40	eqeq2d	$⊢ r = 1_{D} \to (H (x) = G (x) \underset{˙}{\cdot} r \leftrightarrow H (x) = G (x) \underset{˙}{\cdot} 1_{D})$
42	41	ralbidv	$⊢ r = 1_{D} \to (\forall x \in V H (x) = G (x) \underset{˙}{\cdot} r \leftrightarrow \forall x \in V H (x) = G (x) \underset{˙}{\cdot} 1_{D})$
43	42	rspcev	$⊢ (1_{D} \in K \land \forall x \in V H (x) = G (x) \underset{˙}{\cdot} 1_{D}) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
44	14 39 43	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G = V \times \{0_{D}\}) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
45		simpl1	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to W \in LVec$
46		simpl2l	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to G \in F$
47		simpr	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to G \neq V \times \{0_{D}\}$
48	1 26 12 4 5	lfl1	$⊢ (W \in LVec \land G \in F \land G \neq V \times \{0_{D}\}) \to \exists z \in V G (z) = 1_{D}$
49	45 46 47 48	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to \exists z \in V G (z) = 1_{D}$
50		simpl1	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to W \in LVec$
51		simpl2r	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to H \in F$
52		simpr2	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to z \in V$
53	1 2 4 5	lflcl	$⊢ (W \in LVec \land H \in F \land z \in V) \to H (z) \in K$
54	50 51 52 53	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to H (z) \in K$
55		simp11	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to W \in LVec$
56	55 8	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to W \in LMod$
57		simp12r	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H \in F$
58		simp12l	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G \in F$
59		simp3	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to x \in V$
60	1 2 4 5	lflcl	$⊢ (W \in LMod \land G \in F \land x \in V) \to G (x) \in K$
61	56 58 59 60	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \in K$
62		simp22	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to z \in V$
63		eqid	$⊢ \cdot_{W} = \cdot_{W}$
64	1 2 3 4 63 5	lflmul	$⊢ (W \in LMod \land H \in F \land (G (x) \in K \land z \in V)) \to H (G (x) \cdot_{W} z) = G (x) \underset{˙}{\cdot} H (z)$
65	56 57 61 62 64	syl112anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (G (x) \cdot_{W} z) = G (x) \underset{˙}{\cdot} H (z)$
66	65	oveq2d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x) -_{D} H (G (x) \cdot_{W} z) = H (x) -_{D} (G (x) \underset{˙}{\cdot} H (z))$
67	4 1 63 2	lmodvscl	$⊢ (W \in LMod \land G (x) \in K \land z \in V) \to G (x) \cdot_{W} z \in V$
68	56 61 62 67	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \cdot_{W} z \in V$
69		eqid	$⊢ -_{D} = -_{D}$
70		eqid	$⊢ -_{W} = -_{W}$
71	1 69 4 70 5	lflsub	$⊢ (W \in LMod \land H \in F \land (x \in V \land G (x) \cdot_{W} z \in V)) \to H (x -_{W} (G (x) \cdot_{W} z)) = H (x) -_{D} H (G (x) \cdot_{W} z)$
72	56 57 59 68 71	syl112anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x -_{W} (G (x) \cdot_{W} z)) = H (x) -_{D} H (G (x) \cdot_{W} z)$
73	4 70	lmodvsubcl	$⊢ (W \in LMod \land x \in V \land G (x) \cdot_{W} z \in V) \to x -_{W} (G (x) \cdot_{W} z) \in V$
74	56 59 68 73	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to x -_{W} (G (x) \cdot_{W} z) \in V$
75	1 69 4 70 5	lflsub	$⊢ (W \in LMod \land G \in F \land (x \in V \land G (x) \cdot_{W} z \in V)) \to G (x -_{W} (G (x) \cdot_{W} z)) = G (x) -_{D} G (G (x) \cdot_{W} z)$
76	56 58 59 68 75	syl112anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x -_{W} (G (x) \cdot_{W} z)) = G (x) -_{D} G (G (x) \cdot_{W} z)$
77	55 58 59 19	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \in K$
78	1 2 3 4 63 5	lflmul	$⊢ (W \in LMod \land G \in F \land (G (x) \in K \land z \in V)) \to G (G (x) \cdot_{W} z) = G (x) \underset{˙}{\cdot} G (z)$
79	56 58 77 62 78	syl112anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (G (x) \cdot_{W} z) = G (x) \underset{˙}{\cdot} G (z)$
80		simp23	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (z) = 1_{D}$
81	80	oveq2d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \underset{˙}{\cdot} G (z) = G (x) \underset{˙}{\cdot} 1_{D}$
82	55 10	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to D \in Ring$
83	82 77 21	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \underset{˙}{\cdot} 1_{D} = G (x)$
84	79 81 83	3eqtrd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (G (x) \cdot_{W} z) = G (x)$
85	84	oveq2d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) -_{D} G (G (x) \cdot_{W} z) = G (x) -_{D} G (x)$
86	1	lmodfgrp	$⊢ W \in LMod \to D \in Grp$
87	8 86	syl	$⊢ W \in LVec \to D \in Grp$
88	55 87	syl	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to D \in Grp$
89	2 26 69	grpsubid	$⊢ (D \in Grp \land G (x) \in K) \to G (x) -_{D} G (x) = 0_{D}$
90	88 77 89	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) -_{D} G (x) = 0_{D}$
91	76 85 90	3eqtrd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}$
92	4 1 26 5 6	ellkr	$⊢ (W \in LVec \land G \in F) \to (x -_{W} (G (x) \cdot_{W} z) \in L (G) \leftrightarrow (x -_{W} (G (x) \cdot_{W} z) \in V \land G (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}))$
93	55 58 92	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to (x -_{W} (G (x) \cdot_{W} z) \in L (G) \leftrightarrow (x -_{W} (G (x) \cdot_{W} z) \in V \land G (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}))$
94	74 91 93	mpbir2and	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to x -_{W} (G (x) \cdot_{W} z) \in L (G)$
95		simp13	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to L (G) = L (H)$
96	94 95	eleqtrd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to x -_{W} (G (x) \cdot_{W} z) \in L (H)$
97	4 1 26 5 6	ellkr	$⊢ (W \in LVec \land H \in F) \to (x -_{W} (G (x) \cdot_{W} z) \in L (H) \leftrightarrow (x -_{W} (G (x) \cdot_{W} z) \in V \land H (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}))$
98	55 57 97	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to (x -_{W} (G (x) \cdot_{W} z) \in L (H) \leftrightarrow (x -_{W} (G (x) \cdot_{W} z) \in V \land H (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}))$
99	96 98	mpbid	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to (x -_{W} (G (x) \cdot_{W} z) \in V \land H (x -_{W} (G (x) \cdot_{W} z)) = 0_{D})$
100	99	simprd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x -_{W} (G (x) \cdot_{W} z)) = 0_{D}$
101	72 100	eqtr3d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x) -_{D} H (G (x) \cdot_{W} z) = 0_{D}$
102	66 101	eqtr3d	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x) -_{D} (G (x) \underset{˙}{\cdot} H (z)) = 0_{D}$
103	1 2 4 5	lflcl	$⊢ (W \in LVec \land H \in F \land x \in V) \to H (x) \in K$
104	55 57 59 103	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x) \in K$
105	54	3adant3	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (z) \in K$
106	1 2 3	lmodmcl	$⊢ (W \in LMod \land G (x) \in K \land H (z) \in K) \to G (x) \underset{˙}{\cdot} H (z) \in K$
107	56 77 105 106	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to G (x) \underset{˙}{\cdot} H (z) \in K$
108	2 26 69	grpsubeq0	$⊢ (D \in Grp \land H (x) \in K \land G (x) \underset{˙}{\cdot} H (z) \in K) \to (H (x) -_{D} (G (x) \underset{˙}{\cdot} H (z)) = 0_{D} \leftrightarrow H (x) = G (x) \underset{˙}{\cdot} H (z))$
109	88 104 107 108	syl3anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to (H (x) -_{D} (G (x) \underset{˙}{\cdot} H (z)) = 0_{D} \leftrightarrow H (x) = G (x) \underset{˙}{\cdot} H (z))$
110	102 109	mpbid	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D}) \land x \in V) \to H (x) = G (x) \underset{˙}{\cdot} H (z)$
111	110	3expia	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to (x \in V \to H (x) = G (x) \underset{˙}{\cdot} H (z))$
112	111	ralrimiv	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to \forall x \in V H (x) = G (x) \underset{˙}{\cdot} H (z)$
113		oveq2	$⊢ r = H (z) \to G (x) \underset{˙}{\cdot} r = G (x) \underset{˙}{\cdot} H (z)$
114	113	eqeq2d	$⊢ r = H (z) \to (H (x) = G (x) \underset{˙}{\cdot} r \leftrightarrow H (x) = G (x) \underset{˙}{\cdot} H (z))$
115	114	ralbidv	$⊢ r = H (z) \to (\forall x \in V H (x) = G (x) \underset{˙}{\cdot} r \leftrightarrow \forall x \in V H (x) = G (x) \underset{˙}{\cdot} H (z))$
116	115	rspcev	$⊢ (H (z) \in K \land \forall x \in V H (x) = G (x) \underset{˙}{\cdot} H (z)) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
117	54 112 116	syl2anc	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land (G \neq V \times \{0_{D}\} \land z \in V \land G (z) = 1_{D})) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
118	117	3exp2	$⊢ (W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \to (G \neq V \times \{0_{D}\} \to (z \in V \to (G (z) = 1_{D} \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r)))$
119	118	imp	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to (z \in V \to (G (z) = 1_{D} \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r))$
120	119	rexlimdv	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to (\exists z \in V G (z) = 1_{D} \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r)$
121	49 120	mpd	$⊢ ((W \in LVec \land (G \in F \land H \in F) \land L (G) = L (H)) \land G \neq V \times \{0_{D}\}) \to \exists r \in K \forall x \in V H (x) = G (x) \underset{˙}{\cdot} r$
122	44 121	pm2.61dane	$⊢ (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$

Metamath Proof Explorer

Theorem eqlkr

Proof