This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqlkr

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

Ref Expression
Hypotheses eqlkr.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
eqlkr.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
eqlkr.t ⊢ · = ( .r ‘ 𝐷 )
eqlkr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
eqlkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
eqlkr.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
Assertion eqlkr ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · 𝑟 ) )

Proof

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