Theorem eqlkr 39099

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 1192	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
2		lveclmod 21020	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3		eqlkr.d	. . . . . . 7 ⊢ 𝐷 = (Scalar‘𝑊)
4	3	lmodring 20781	. . . . . 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 2730	. . . . 5 ⊢ (1r‘𝐷) = (1r‘𝐷)
9	7, 8	ringidcl 20181	. . . 4 ⊢ (𝐷 ∈ Ring → (1r‘𝐷) ∈ 𝐾)
10	6, 9	syl 17	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (1r‘𝐷) ∈ 𝐾)
11		simp11 1204	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
12	11, 5	syl 17	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
13		simp12l 1287	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
14		simp3 1138	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
15		eqlkr.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
16		eqlkr.f	. . . . . . . . 9 ⊢ 𝐹 = (LFnl‘𝑊)
17	3, 7, 15, 16	lflcl 39064	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
18	11, 13, 14, 17	syl3anc 1373	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
19		eqlkr.t	. . . . . . . 8 ⊢ · = (.r‘𝐷)
20	7, 19, 8	ringridm 20186	. . . . . . 7 ⊢ ((𝐷 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
21	12, 18, 20	syl2anc 584	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
22		simp2 1137	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = (𝑉 × {(0g‘𝐷)}))
23		simp13 1206	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
24	11, 2	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
25		eqid 2730	. . . . . . . . . . . . 13 ⊢ (0g‘𝐷) = (0g‘𝐷)
26		eqlkr.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LKer‘𝑊)
27	3, 25, 15, 16, 26	lkr0f 39094	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
28	24, 13, 27	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
29	22, 28	mpbird 257	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = 𝑉)
30	23, 29	eqtr3d 2767	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐻) = 𝑉)
31		simp12r 1288	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
32	3, 25, 15, 16, 26	lkr0f 39094	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
33	24, 31, 32	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
34	30, 33	mpbid 232	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 = (𝑉 × {(0g‘𝐷)}))
35	22, 34	eqtr4d 2768	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = 𝐻)
36	35	fveq1d 6863	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥))
37	21, 36	eqtr2d 2766	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
38	37	3expia 1121	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
39	38	ralrimiv 3125	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
40		oveq2 7398	. . . . . 6 ⊢ (𝑟 = (1r‘𝐷) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (1r‘𝐷)))
41	40	eqeq2d 2741	. . . . 5 ⊢ (𝑟 = (1r‘𝐷) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
42	41	ralbidv 3157	. . . 4 ⊢ (𝑟 = (1r‘𝐷) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
43	42	rspcev 3591	. . 3 ⊢ (((1r‘𝐷) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
44	10, 39, 43	syl2anc 584	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
45		simpl1 1192	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
46		simpl2l 1227	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ∈ 𝐹)
47		simpr 484	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))
48	3, 25, 8, 15, 16	lfl1 39070	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
49	45, 46, 47, 48	syl3anc 1373	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
50		simpl1 1192	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑊 ∈ LVec)
51		simpl2r 1228	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝐻 ∈ 𝐹)
52		simpr2 1196	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑧 ∈ 𝑉)
53	3, 7, 15, 16	lflcl 39064	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
54	50, 51, 52, 53	syl3anc 1373	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝐻‘𝑧) ∈ 𝐾)
55		simp11 1204	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
56	55, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
57		simp12r 1288	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
58		simp12l 1287	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
59		simp3 1138	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
60	3, 7, 15, 16	lflcl 39064	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
61	56, 58, 59, 60	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
62		simp22 1208	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑧 ∈ 𝑉)
63		eqid 2730	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
64	3, 7, 19, 15, 63, 16	lflmul 39068	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
65	56, 57, 61, 62, 64	syl112anc 1376	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
66	65	oveq2d 7406	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))))
67	15, 3, 63, 7	lmodvscl 20791	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
68	56, 61, 62, 67	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
69		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (-g‘𝐷) = (-g‘𝐷)
70		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (-g‘𝑊) = (-g‘𝑊)
71	3, 69, 15, 70, 16	lflsub 39067	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
72	56, 57, 59, 68, 71	syl112anc 1376	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
73	15, 70	lmodvsubcl 20820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
74	56, 59, 68, 73	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
75	3, 69, 15, 70, 16	lflsub 39067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
76	56, 58, 59, 68, 75	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
77	55, 58, 59, 17	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
78	3, 7, 19, 15, 63, 16	lflmul 39068	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
79	56, 58, 77, 62, 78	syl112anc 1376	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
80		simp23 1209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑧) = (1r‘𝐷))
81	80	oveq2d 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐺‘𝑧)) = ((𝐺‘𝑥) · (1r‘𝐷)))
82	55, 5	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
83	82, 77, 20	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
84	79, 81, 83	3eqtrd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = (𝐺‘𝑥))
85	84	oveq2d 7406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)))
86	3	lmodfgrp 20782	. . . . . . . . . . . . . . . . . . . 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 18963	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
90	88, 77, 89	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
91	76, 85, 90	3eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
92	15, 3, 25, 16, 26	ellkr 39089	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
93	55, 58, 92	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
94	74, 91, 93	mpbir2and 713	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺))
95		simp13 1206	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
96	94, 95	eleqtrd 2831	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻))
97	15, 3, 25, 16, 26	ellkr 39089	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
98	55, 57, 97	syl2anc 584	. . . . . . . . . . . . . 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 2767	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
102	66, 101	eqtr3d 2767	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷))
103	3, 7, 15, 16	lflcl 39064	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
104	55, 57, 59, 103	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
105	54	3adant3 1132	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
106	3, 7, 19	lmodmcl 20786	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ (𝐻‘𝑧) ∈ 𝐾) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
107	56, 77, 105, 106	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
108	7, 25, 69	grpsubeq0 18965	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Grp ∧ (𝐻‘𝑥) ∈ 𝐾 ∧ ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
109	88, 104, 107, 108	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
110	102, 109	mpbid 232	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
111	110	3expia 1121	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
112	111	ralrimiv 3125	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
113		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
114	113	eqeq2d 2741	. . . . . . . . 9 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
115	114	ralbidv 3157	. . . . . . . 8 ⊢ (𝑟 = (𝐻‘𝑧) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
116	115	rspcev 3591	. . . . . . 7 ⊢ (((𝐻‘𝑧) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
117	54, 112, 116	syl2anc 584	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
118	117	3exp2 1355	. . . . 5 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))))
119	118	imp 406	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))))
120	119	rexlimdv 3133	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))
121	49, 120	mpd 15	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
122	44, 121	pm2.61dane 3013	1 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  {csn 4592   × cxp 5639  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  0_gc0g 17409  Grpcgrp 18872  -_gcsg 18874  1_rcur 20097  Ringcrg 20149  LModclmod 20773  LVecclvec 21016  LFnlclfn 39057  LKerclk 39085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-3 12257  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-0g 17411  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875  df-minusg 18876  df-sbg 18877  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-ring 20151  df-oppr 20253  df-dvdsr 20273  df-unit 20274  df-invr 20304  df-drng 20647  df-lmod 20775  df-lvec 21017  df-lfl 39058  df-lkr 39086

This theorem is referenced by:  eqlkr2  39100  eqlkr3  39101