Theorem eqlkr 34386

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 1064	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
2		lveclmod 19106	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3		eqlkr.d	. . . . . . 7 ⊢ 𝐷 = (Scalar‘𝑊)
4	3	lmodring 18871	. . . . . 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 2622	. . . . 5 ⊢ (1r‘𝐷) = (1r‘𝐷)
9	7, 8	ringidcl 18568	. . . 4 ⊢ (𝐷 ∈ Ring → (1r‘𝐷) ∈ 𝐾)
10	6, 9	syl 17	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (1r‘𝐷) ∈ 𝐾)
11		simp11 1091	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
12	11, 5	syl 17	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
13		simp12l 1174	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
14		simp3 1063	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
15		eqlkr.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
16		eqlkr.f	. . . . . . . . 9 ⊢ 𝐹 = (LFnl‘𝑊)
17	3, 7, 15, 16	lflcl 34351	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
18	11, 13, 14, 17	syl3anc 1326	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
19		eqlkr.t	. . . . . . . 8 ⊢ · = (.r‘𝐷)
20	7, 19, 8	ringridm 18572	. . . . . . 7 ⊢ ((𝐷 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
21	12, 18, 20	syl2anc 693	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
22		simp2 1062	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = (𝑉 × {(0g‘𝐷)}))
23		simp13 1093	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
24	11, 2	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
25		eqid 2622	. . . . . . . . . . . . 13 ⊢ (0g‘𝐷) = (0g‘𝐷)
26		eqlkr.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (LKer‘𝑊)
27	3, 25, 15, 16, 26	lkr0f 34381	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
28	24, 13, 27	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)})))
29	22, 28	mpbird 247	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = 𝑉)
30	23, 29	eqtr3d 2658	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐻) = 𝑉)
31		simp12r 1175	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
32	3, 25, 15, 16, 26	lkr0f 34381	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
33	24, 31, 32	syl2anc 693	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝐻) = 𝑉 ↔ 𝐻 = (𝑉 × {(0g‘𝐷)})))
34	30, 33	mpbid 222	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐻 = (𝑉 × {(0g‘𝐷)}))
35	22, 34	eqtr4d 2659	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → 𝐺 = 𝐻)
36	35	fveq1d 6193	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) = (𝐻‘𝑥))
37	21, 36	eqtr2d 2657	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)}) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
38	37	3expia 1267	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
39	38	ralrimiv 2965	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷)))
40		oveq2 6658	. . . . . 6 ⊢ (𝑟 = (1r‘𝐷) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (1r‘𝐷)))
41	40	eqeq2d 2632	. . . . 5 ⊢ (𝑟 = (1r‘𝐷) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
42	41	ralbidv 2986	. . . 4 ⊢ (𝑟 = (1r‘𝐷) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))))
43	42	rspcev 3309	. . 3 ⊢ (((1r‘𝐷) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
44	10, 39, 43	syl2anc 693	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
45		simpl1 1064	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LVec)
46		simpl2l 1114	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ∈ 𝐹)
47		simpr 477	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))
48	3, 25, 8, 15, 16	lfl1 34357	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
49	45, 46, 47, 48	syl3anc 1326	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷))
50		simpl1 1064	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑊 ∈ LVec)
51		simpl2r 1115	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝐻 ∈ 𝐹)
52		simpr2 1068	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → 𝑧 ∈ 𝑉)
53	3, 7, 15, 16	lflcl 34351	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
54	50, 51, 52, 53	syl3anc 1326	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝐻‘𝑧) ∈ 𝐾)
55		simp11 1091	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LVec)
56	55, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑊 ∈ LMod)
57		simp12r 1175	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐻 ∈ 𝐹)
58		simp12l 1174	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐺 ∈ 𝐹)
59		simp3 1063	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
60	3, 7, 15, 16	lflcl 34351	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
61	56, 58, 59, 60	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
62		simp22 1095	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝑧 ∈ 𝑉)
63		eqid 2622	. . . . . . . . . . . . . 14 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
64	3, 7, 19, 15, 63, 16	lflmul 34355	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
65	56, 57, 61, 62, 64	syl112anc 1330	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
66	65	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))))
67	15, 3, 63, 7	lmodvscl 18880	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
68	56, 61, 62, 67	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)
69		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (-g‘𝐷) = (-g‘𝐷)
70		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (-g‘𝑊) = (-g‘𝑊)
71	3, 69, 15, 70, 16	lflsub 34354	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
72	56, 57, 59, 68, 71	syl112anc 1330	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
73	15, 70	lmodvsubcl 18908	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
74	56, 59, 68, 73	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉)
75	3, 69, 15, 70, 16	lflsub 34354	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑥 ∈ 𝑉 ∧ ((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧) ∈ 𝑉)) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
76	56, 58, 59, 68, 75	syl112anc 1330	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))))
77	55, 58, 59, 17	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑥) ∈ 𝐾)
78	3, 7, 19, 15, 63, 16	lflmul 34355	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((𝐺‘𝑥) ∈ 𝐾 ∧ 𝑧 ∈ 𝑉)) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
79	56, 58, 77, 62, 78	syl112anc 1330	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = ((𝐺‘𝑥) · (𝐺‘𝑧)))
80		simp23 1096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘𝑧) = (1r‘𝐷))
81	80	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐺‘𝑧)) = ((𝐺‘𝑥) · (1r‘𝐷)))
82	55, 5	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → 𝐷 ∈ Ring)
83	82, 77, 20	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (1r‘𝐷)) = (𝐺‘𝑥))
84	79, 81, 83	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) = (𝐺‘𝑥))
85	84	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)))
86	3	lmodfgrp 18872	. . . . . . . . . . . . . . . . . . . 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 17499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑥) ∈ 𝐾) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
90	88, 77, 89	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥)(-g‘𝐷)(𝐺‘𝑥)) = (0g‘𝐷))
91	76, 85, 90	3eqtrd 2660	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
92	15, 3, 25, 16, 26	ellkr 34376	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
93	55, 58, 92	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐺‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
94	74, 91, 93	mpbir2and 957	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐺))
95		simp13 1093	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝐺) = (𝐿‘𝐻))
96	94, 95	eleqtrd 2703	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻))
97	15, 3, 25, 16, 26	ellkr 34376	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
98	55, 57, 97	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ (𝐿‘𝐻) ↔ ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))))
99	96, 98	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧)) ∈ 𝑉 ∧ (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷)))
100	99	simprd 479	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘(𝑥(-g‘𝑊)((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
101	72, 100	eqtr3d 2658	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)(𝐻‘((𝐺‘𝑥)( ·𝑠 ‘𝑊)𝑧))) = (0g‘𝐷))
102	66, 101	eqtr3d 2658	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷))
103	3, 7, 15, 16	lflcl 34351	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
104	55, 57, 59, 103	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) ∈ 𝐾)
105	54	3adant3 1081	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑧) ∈ 𝐾)
106	3, 7, 19	lmodmcl 18875	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ (𝐺‘𝑥) ∈ 𝐾 ∧ (𝐻‘𝑧) ∈ 𝐾) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
107	56, 77, 105, 106	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾)
108	7, 25, 69	grpsubeq0 17501	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Grp ∧ (𝐻‘𝑥) ∈ 𝐾 ∧ ((𝐺‘𝑥) · (𝐻‘𝑧)) ∈ 𝐾) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
109	88, 104, 107, 108	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (((𝐻‘𝑥)(-g‘𝐷)((𝐺‘𝑥) · (𝐻‘𝑧))) = (0g‘𝐷) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
110	102, 109	mpbid 222	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷)) ∧ 𝑥 ∈ 𝑉) → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
111	110	3expia 1267	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → (𝑥 ∈ 𝑉 → (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
112	111	ralrimiv 2965	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
113		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐺‘𝑥) · 𝑟) = ((𝐺‘𝑥) · (𝐻‘𝑧)))
114	113	eqeq2d 2632	. . . . . . . . 9 ⊢ (𝑟 = (𝐻‘𝑧) → ((𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
115	114	ralbidv 2986	. . . . . . . 8 ⊢ (𝑟 = (𝐻‘𝑧) → (∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟) ↔ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))))
116	115	rspcev 3309	. . . . . . 7 ⊢ (((𝐻‘𝑧) ∈ 𝐾 ∧ ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑧))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
117	54, 112, 116	syl2anc 693	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝑧 ∈ 𝑉 ∧ (𝐺‘𝑧) = (1r‘𝐷))) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
118	117	3exp2 1285	. . . . 5 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → (𝐺 ≠ (𝑉 × {(0g‘𝐷)}) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))))
119	118	imp 445	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (𝑧 ∈ 𝑉 → ((𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))))
120	119	rexlimdv 3030	. . 3 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (∃𝑧 ∈ 𝑉 (𝐺‘𝑧) = (1r‘𝐷) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)))
121	49, 120	mpd 15	. 2 ⊢ (((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))
122	44, 121	pm2.61dane 2881	1 ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {csn 4177   × cxp 5112  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  ._rcmulr 15942  Scalarcsca 15944   ·_𝑠 cvsca 15945  0_gc0g 16100  Grpcgrp 17422  -_gcsg 17424  1_rcur 18501  Ringcrg 18547  LModclmod 18863  LVecclvec 19102  LFnlclfn 34344  LKerclk 34372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-minusg 17426  df-sbg 17427  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-drng 18749  df-lmod 18865  df-lvec 19103  df-lfl 34345  df-lkr 34373

This theorem is referenced by:  eqlkr2  34387  eqlkr3  34388