Theorem eqlkr 39479

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

Hypotheses

Ref	Expression
eqlkr.d	⊢ 𝐷 = (Scalar‘𝑊)
eqlkr.k	⊢ 𝐾 = (Base‘𝐷)
eqlkr.t	⊢ · = (.r‘𝐷)
eqlkr.v	⊢ 𝑉 = (Base‘𝑊)
eqlkr.f	⊢ 𝐹 = (LFnl‘𝑊)
eqlkr.l	⊢ 𝐿 = (LKer‘𝑊)

Assertion

Ref	Expression
eqlkr	⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Distinct variable groups:   𝑥,𝑟,𝐷   𝑥,𝐹   𝐺,𝑟,𝑥   𝐻,𝑟,𝑥   𝑉,𝑟,𝑥   𝐾,𝑟   𝑥,𝐿   · ,𝑟   𝑥,𝑊

Allowed substitution hints:   · (𝑥)   𝐹(𝑟)   𝐾(𝑥)   𝐿(𝑟)   𝑊(𝑟)

Proof of Theorem eqlkr

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1193	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
2		lveclmod 21073	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3		eqlkr.d	. . . . . . 7 ⊢ 𝐷 = (Scalar‘𝑊)
4	3	lmodring 20834	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝐷 ∈ Ring)
5	2, 4	syl 17	. . . . 5 ⊢ (𝑊 ∈ LVec → 𝐷 ∈ Ring)
6	1, 5	syl 17	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → 𝐷 ∈ Ring)
7		eqlkr.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐷)
8		eqid 2737	. . . . 5 ⊢ (1r‘𝐷) = (1r‘𝐷)
9	7, 8	ringidcl 20215	. . . 4 ⊢ (𝐷 ∈ Ring → (1r‘𝐷) ∈ 𝐾)
10	6, 9	syl 17	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (1r‘𝐷) ∈ 𝐾)
11		simp11 1205	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
12	11, 5	syl 17	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
13		simp12l 1288	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
14		simp3 1139	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
15		eqlkr.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
16		eqlkr.f	. . . . . . . . 9 ⊢ 𝐹 = (LFnl‘𝑊)
17	3, 7, 15, 16	lflcl 39444	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
18	11, 13, 14, 17	syl3anc 1374	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
19		eqlkr.t	. . . . . . . 8 ⊢ · = (.r‘𝐷)
20	7, 19, 8	ringridm 20220	. . . . . . 7 ⊢ ((𝐷 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
21	12, 18, 20	syl2anc 585	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
22		simp2 1138	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = (𝑉 × {(0g‘𝐷)}))
23		simp13 1207	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
24	11, 2	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
25		eqid 2737	. . . . . . . . . . . . 13 ⊢ (0g‘𝐷) = (0g‘𝐷)
26		eqlkr.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LKer‘𝑊)
27	3, 25, 15, 16, 26	lkr0f 39474	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
28	24, 13, 27	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
29	22, 28	mpbird 257	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = 𝑉)
30	23, 29	eqtr3d 2774	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐻) = 𝑉)
31		simp12r 1289	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
32	3, 25, 15, 16, 26	lkr0f 39474	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
33	24, 31, 32	syl2anc 585	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
34	30, 33	mpbid 232	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 = (𝑉 × {(0g‘𝐷)}))
35	22, 34	eqtr4d 2775	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = 𝐻)
36	35	fveq1d 6844	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥))
37	21, 36	eqtr2d 2773	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
38	37	3expia 1122	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
39	38	ralrimiv 3129	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
40		oveq2 7376	. . . . . 6 ⊢ (𝑟 = (1r‘𝐷) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (1r‘𝐷)))
41	40	eqeq2d 2748	. . . . 5 ⊢ (𝑟 = (1r‘𝐷) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
42	41	ralbidv 3161	. . . 4 ⊢ (𝑟 = (1r‘𝐷) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
43	42	rspcev 3578	. . 3 ⊢ (((1r‘𝐷) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
44	10, 39, 43	syl2anc 585	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
45		simpl1 1193	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
46		simpl2l 1228	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ∈ 𝐹)
47		simpr 484	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))
48	3, 25, 8, 15, 16	lfl1 39450	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
49	45, 46, 47, 48	syl3anc 1374	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
50		simpl1 1193	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑊 ∈ LVec)
51		simpl2r 1229	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝐻 ∈ 𝐹)
52		simpr2 1197	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑧 ∈ 𝑉)
53	3, 7, 15, 16	lflcl 39444	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
54	50, 51, 52, 53	syl3anc 1374	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝐻‘𝑧) ∈ 𝐾)
55		simp11 1205	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
56	55, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
57		simp12r 1289	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
58		simp12l 1288	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
59		simp3 1139	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
60	3, 7, 15, 16	lflcl 39444	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
61	56, 58, 59, 60	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
62		simp22 1209	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑧 ∈ 𝑉)
63		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
64	3, 7, 19, 15, 63, 16	lflmul 39448	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
65	56, 57, 61, 62, 64	syl112anc 1377	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
66	65	oveq2d 7384	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))))
67	15, 3, 63, 7	lmodvscl 20844	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
68	56, 61, 62, 67	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
69		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (-g‘𝐷) = (-g‘𝐷)
70		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (-g‘𝑊) = (-g‘𝑊)
71	3, 69, 15, 70, 16	lflsub 39447	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
72	56, 57, 59, 68, 71	syl112anc 1377	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
73	15, 70	lmodvsubcl 20873	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
74	56, 59, 68, 73	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
75	3, 69, 15, 70, 16	lflsub 39447	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
76	56, 58, 59, 68, 75	syl112anc 1377	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
77	55, 58, 59, 17	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
78	3, 7, 19, 15, 63, 16	lflmul 39448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
79	56, 58, 77, 62, 78	syl112anc 1377	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
80		simp23 1210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑧) = (1r‘𝐷))
81	80	oveq2d 7384	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐺‘𝑧)) = ((𝐺‘𝑥) · (1r‘𝐷)))
82	55, 5	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
83	82, 77, 20	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
84	79, 81, 83	3eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = (𝐺‘𝑥))
85	84	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)))
86	3	lmodfgrp 20835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ LMod → 𝐷 ∈ Grp)
87	2, 86	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ∈ LVec → 𝐷 ∈ Grp)
88	55, 87	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Grp)
89	7, 25, 69	grpsubid 18969	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
90	88, 77, 89	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
91	76, 85, 90	3eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
92	15, 3, 25, 16, 26	ellkr 39469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
93	55, 58, 92	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
94	74, 91, 93	mpbir2and 714	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺))
95		simp13 1207	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
96	94, 95	eleqtrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻))
97	15, 3, 25, 16, 26	ellkr 39469	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
98	55, 57, 97	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
99	96, 98	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷)))
100	99	simprd 495	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
101	72, 100	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
102	66, 101	eqtr3d 2774	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷))
103	3, 7, 15, 16	lflcl 39444	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
104	55, 57, 59, 103	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
105	54	3adant3 1133	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
106	3, 7, 19	lmodmcl 20839	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ (𝐻‘𝑧) ∈ 𝐾) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
107	56, 77, 105, 106	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
108	7, 25, 69	grpsubeq0 18971	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Grp ∧ (𝐻‘𝑥) ∈ 𝐾 ∧ ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
109	88, 104, 107, 108	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
110	102, 109	mpbid 232	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
111	110	3expia 1122	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
112	111	ralrimiv 3129	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
113		oveq2 7376	. . . . . . . . . 10 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
114	113	eqeq2d 2748	. . . . . . . . 9 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
115	114	ralbidv 3161	. . . . . . . 8 ⊢ (𝑟 = (𝐻‘𝑧) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
116	115	rspcev 3578	. . . . . . 7 ⊢ (((𝐻‘𝑧) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
117	54, 112, 116	syl2anc 585	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
118	117	3exp2 1356	. . . . 5 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))))
119	118	imp 406	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))))
120	119	rexlimdv 3137	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))
121	49, 120	mpd 15	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
122	44, 121	pm2.61dane 3020	1 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {csn 4582   × cxp 5630  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  0_gc0g 17371  Grpcgrp 18878  -_gcsg 18880  1_rcur 20131  Ringcrg 20183  LModclmod 20826  LVecclvec 21069  LFnlclfn 39437  LKerclk 39465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-3 12221  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18881  df-minusg 18882  df-sbg 18883  df-cmn 19726  df-abl 19727  df-mgp 20091  df-rng 20103  df-ur 20132  df-ring 20185  df-oppr 20288  df-dvdsr 20308  df-unit 20309  df-invr 20339  df-drng 20679  df-lmod 20828  df-lvec 21070  df-lfl 39438  df-lkr 39466

This theorem is referenced by:  eqlkr2  39480  eqlkr3  39481