Theorem eqlkr 39085

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 21045	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3		eqlkr.d	. . . . . . 7 ⊢ 𝐷 = (Scalar‘𝑊)
4	3	lmodring 20806	. . . . . 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 2729	. . . . 5 ⊢ (1r‘𝐷) = (1r‘𝐷)
9	7, 8	ringidcl 20185	. . . 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 39050	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
18	11, 13, 14, 17	syl3anc 1373	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
19		eqlkr.t	. . . . . . . 8 ⊢ · = (.r‘𝐷)
20	7, 19, 8	ringridm 20190	. . . . . . 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 2729	. . . . . . . . . . . . 13 ⊢ (0g‘𝐷) = (0g‘𝐷)
26		eqlkr.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LKer‘𝑊)
27	3, 25, 15, 16, 26	lkr0f 39080	. . . . . . . . . . . 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 2766	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐻) = 𝑉)
31		simp12r 1288	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
32	3, 25, 15, 16, 26	lkr0f 39080	. . . . . . . . . 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 2767	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = 𝐻)
36	35	fveq1d 6842	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥))
37	21, 36	eqtr2d 2765	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
38	37	3expia 1121	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
39	38	ralrimiv 3124	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
40		oveq2 7377	. . . . . 6 ⊢ (𝑟 = (1r‘𝐷) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (1r‘𝐷)))
41	40	eqeq2d 2740	. . . . 5 ⊢ (𝑟 = (1r‘𝐷) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
42	41	ralbidv 3156	. . . 4 ⊢ (𝑟 = (1r‘𝐷) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
43	42	rspcev 3585	. . 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 39056	. . . 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 39050	. . . . . . . 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 39050	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
61	56, 58, 59, 60	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
62		simp22 1208	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑧 ∈ 𝑉)
63		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
64	3, 7, 19, 15, 63, 16	lflmul 39054	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
65	56, 57, 61, 62, 64	syl112anc 1376	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
66	65	oveq2d 7385	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))))
67	15, 3, 63, 7	lmodvscl 20816	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
68	56, 61, 62, 67	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
69		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (-g‘𝐷) = (-g‘𝐷)
70		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (-g‘𝑊) = (-g‘𝑊)
71	3, 69, 15, 70, 16	lflsub 39053	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
72	56, 57, 59, 68, 71	syl112anc 1376	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
73	15, 70	lmodvsubcl 20845	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
74	56, 59, 68, 73	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
75	3, 69, 15, 70, 16	lflsub 39053	. . . . . . . . . . . . . . . . . 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 39054	. . . . . . . . . . . . . . . . . . . 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 7385	. . . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = (𝐺‘𝑥))
85	84	oveq2d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)))
86	3	lmodfgrp 20807	. . . . . . . . . . . . . . . . . . . 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 18938	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
90	88, 77, 89	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
91	76, 85, 90	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
92	15, 3, 25, 16, 26	ellkr 39075	. . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻))
97	15, 3, 25, 16, 26	ellkr 39075	. . . . . . . . . . . . . . 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 2766	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
102	66, 101	eqtr3d 2766	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷))
103	3, 7, 15, 16	lflcl 39050	. . . . . . . . . . . 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 20811	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ (𝐻‘𝑧) ∈ 𝐾) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
107	56, 77, 105, 106	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
108	7, 25, 69	grpsubeq0 18940	. . . . . . . . . . 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 3124	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
113		oveq2 7377	. . . . . . . . . 10 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
114	113	eqeq2d 2740	. . . . . . . . 9 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
115	114	ralbidv 3156	. . . . . . . 8 ⊢ (𝑟 = (𝐻‘𝑧) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
116	115	rspcev 3585	. . . . . . 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 3132	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))
121	49, 120	mpd 15	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
122	44, 121	pm2.61dane 3012	1 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {csn 4585   × cxp 5629  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  ._rcmulr 17197  Scalarcsca 17199   ·_𝑠 cvsca 17200  0_gc0g 17378  Grpcgrp 18847  -_gcsg 18849  1_rcur 20101  Ringcrg 20153  LModclmod 20798  LVecclvec 21041  LFnlclfn 39043  LKerclk 39071

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 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-tpos 8182  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-map 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-2 12225  df-3 12226  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-0g 17380  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-grp 18850  df-minusg 18851  df-sbg 18852  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-ring 20155  df-oppr 20257  df-dvdsr 20277  df-unit 20278  df-invr 20308  df-drng 20651  df-lmod 20800  df-lvec 21042  df-lfl 39044  df-lkr 39072

This theorem is referenced by:  eqlkr2  39086  eqlkr3  39087