Theorem eqlkr 36237

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 1187	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
2		lveclmod 19880	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3		eqlkr.d	. . . . . . 7 ⊢ 𝐷 = (Scalar‘𝑊)
4	3	lmodring 19644	. . . . . 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 2823	. . . . 5 ⊢ (1r‘𝐷) = (1r‘𝐷)
9	7, 8	ringidcl 19320	. . . 4 ⊢ (𝐷 ∈ Ring → (1r‘𝐷) ∈ 𝐾)
10	6, 9	syl 17	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (1r‘𝐷) ∈ 𝐾)
11		simp11 1199	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
12	11, 5	syl 17	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
13		simp12l 1282	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
14		simp3 1134	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
15		eqlkr.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
16		eqlkr.f	. . . . . . . . 9 ⊢ 𝐹 = (LFnl‘𝑊)
17	3, 7, 15, 16	lflcl 36202	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
18	11, 13, 14, 17	syl3anc 1367	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
19		eqlkr.t	. . . . . . . 8 ⊢ · = (.r‘𝐷)
20	7, 19, 8	ringridm 19324	. . . . . . 7 ⊢ ((𝐷 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
21	12, 18, 20	syl2anc 586	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
22		simp2 1133	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = (𝑉 × {(0g‘𝐷)}))
23		simp13 1201	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
24	11, 2	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
25		eqid 2823	. . . . . . . . . . . . 13 ⊢ (0g‘𝐷) = (0g‘𝐷)
26		eqlkr.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LKer‘𝑊)
27	3, 25, 15, 16, 26	lkr0f 36232	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
28	24, 13, 27	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
29	22, 28	mpbird 259	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = 𝑉)
30	23, 29	eqtr3d 2860	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐻) = 𝑉)
31		simp12r 1283	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
32	3, 25, 15, 16, 26	lkr0f 36232	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
33	24, 31, 32	syl2anc 586	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
34	30, 33	mpbid 234	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 = (𝑉 × {(0g‘𝐷)}))
35	22, 34	eqtr4d 2861	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = 𝐻)
36	35	fveq1d 6674	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥))
37	21, 36	eqtr2d 2859	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
38	37	3expia 1117	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
39	38	ralrimiv 3183	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
40		oveq2 7166	. . . . . 6 ⊢ (𝑟 = (1r‘𝐷) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (1r‘𝐷)))
41	40	eqeq2d 2834	. . . . 5 ⊢ (𝑟 = (1r‘𝐷) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
42	41	ralbidv 3199	. . . 4 ⊢ (𝑟 = (1r‘𝐷) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
43	42	rspcev 3625	. . 3 ⊢ (((1r‘𝐷) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
44	10, 39, 43	syl2anc 586	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
45		simpl1 1187	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
46		simpl2l 1222	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ∈ 𝐹)
47		simpr 487	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))
48	3, 25, 8, 15, 16	lfl1 36208	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
49	45, 46, 47, 48	syl3anc 1367	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
50		simpl1 1187	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑊 ∈ LVec)
51		simpl2r 1223	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝐻 ∈ 𝐹)
52		simpr2 1191	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑧 ∈ 𝑉)
53	3, 7, 15, 16	lflcl 36202	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
54	50, 51, 52, 53	syl3anc 1367	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝐻‘𝑧) ∈ 𝐾)
55		simp11 1199	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
56	55, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
57		simp12r 1283	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
58		simp12l 1282	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
59		simp3 1134	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
60	3, 7, 15, 16	lflcl 36202	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
61	56, 58, 59, 60	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
62		simp22 1203	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑧 ∈ 𝑉)
63		eqid 2823	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
64	3, 7, 19, 15, 63, 16	lflmul 36206	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
65	56, 57, 61, 62, 64	syl112anc 1370	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
66	65	oveq2d 7174	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))))
67	15, 3, 63, 7	lmodvscl 19653	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
68	56, 61, 62, 67	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
69		eqid 2823	. . . . . . . . . . . . . 14 ⊢ (-g‘𝐷) = (-g‘𝐷)
70		eqid 2823	. . . . . . . . . . . . . 14 ⊢ (-g‘𝑊) = (-g‘𝑊)
71	3, 69, 15, 70, 16	lflsub 36205	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
72	56, 57, 59, 68, 71	syl112anc 1370	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
73	15, 70	lmodvsubcl 19681	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
74	56, 59, 68, 73	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
75	3, 69, 15, 70, 16	lflsub 36205	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
76	56, 58, 59, 68, 75	syl112anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
77	55, 58, 59, 17	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
78	3, 7, 19, 15, 63, 16	lflmul 36206	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
79	56, 58, 77, 62, 78	syl112anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
80		simp23 1204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑧) = (1r‘𝐷))
81	80	oveq2d 7174	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐺‘𝑧)) = ((𝐺‘𝑥) · (1r‘𝐷)))
82	55, 5	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
83	82, 77, 20	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
84	79, 81, 83	3eqtrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = (𝐺‘𝑥))
85	84	oveq2d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)))
86	3	lmodfgrp 19645	. . . . . . . . . . . . . . . . . . . 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 18185	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
90	88, 77, 89	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
91	76, 85, 90	3eqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
92	15, 3, 25, 16, 26	ellkr 36227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
93	55, 58, 92	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
94	74, 91, 93	mpbir2and 711	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺))
95		simp13 1201	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
96	94, 95	eleqtrd 2917	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻))
97	15, 3, 25, 16, 26	ellkr 36227	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
98	55, 57, 97	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
99	96, 98	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷)))
100	99	simprd 498	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
101	72, 100	eqtr3d 2860	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
102	66, 101	eqtr3d 2860	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷))
103	3, 7, 15, 16	lflcl 36202	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
104	55, 57, 59, 103	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
105	54	3adant3 1128	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
106	3, 7, 19	lmodmcl 19648	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ (𝐻‘𝑧) ∈ 𝐾) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
107	56, 77, 105, 106	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
108	7, 25, 69	grpsubeq0 18187	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Grp ∧ (𝐻‘𝑥) ∈ 𝐾 ∧ ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
109	88, 104, 107, 108	syl3anc 1367	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
110	102, 109	mpbid 234	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
111	110	3expia 1117	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
112	111	ralrimiv 3183	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
113		oveq2 7166	. . . . . . . . . 10 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
114	113	eqeq2d 2834	. . . . . . . . 9 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
115	114	ralbidv 3199	. . . . . . . 8 ⊢ (𝑟 = (𝐻‘𝑧) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
116	115	rspcev 3625	. . . . . . 7 ⊢ (((𝐻‘𝑧) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
117	54, 112, 116	syl2anc 586	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
118	117	3exp2 1350	. . . . 5 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))))
119	118	imp 409	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))))
120	119	rexlimdv 3285	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))
121	49, 120	mpd 15	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
122	44, 121	pm2.61dane 3106	1 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140  ∃wrex 3141  {csn 4569   × cxp 5555  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  ._rcmulr 16568  Scalarcsca 16570   ·_𝑠 cvsca 16571  0_gc0g 16715  Grpcgrp 18105  -_gcsg 18107  1_rcur 19253  Ringcrg 19299  LModclmod 19636  LVecclvec 19876  LFnlclfn 36195  LKerclk 36223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-tpos 7894  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-3 11704  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-0g 16717  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-grp 18108  df-minusg 18109  df-sbg 18110  df-cmn 18910  df-abl 18911  df-mgp 19242  df-ur 19254  df-ring 19301  df-oppr 19375  df-dvdsr 19393  df-unit 19394  df-invr 19424  df-drng 19506  df-lmod 19638  df-lvec 19877  df-lfl 36196  df-lkr 36224

This theorem is referenced by:  eqlkr2  36238  eqlkr3  36239