Metamath Proof Explorer

Theorem eqlkr3

Description: Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses eqlkr3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
eqlkr3.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
eqlkr3.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
eqlkr3.o ⊢ 0 = ( 0g ‘ 𝑆 )
eqlkr3.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
eqlkr3.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
eqlkr3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
eqlkr3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
eqlkr3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
eqlkr3.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
eqlkr3.e ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
eqlkr3.a ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
eqlkr3.n ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
Assertion eqlkr3 ( 𝜑 → 𝐺 = 𝐻 )

Proof

Step Hyp Ref Expression
1 eqlkr3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 eqlkr3.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
3 eqlkr3.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
4 eqlkr3.o ⊢ 0 = ( 0g ‘ 𝑆 )
5 eqlkr3.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 eqlkr3.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
7 eqlkr3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 eqlkr3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 eqlkr3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 eqlkr3.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
11 eqlkr3.e ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )
12 eqlkr3.a ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
13 eqlkr3.n ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
14 2 3 1 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝑅 )
15 7 9 14 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝑅 )
16 15 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
17 2 3 1 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : 𝑉 ⟶ 𝑅 )
18 7 10 17 syl2anc ⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝑅 )
19 18 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
20 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
21 2 3 20 1 5 6 eqlkr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) )
22 7 9 10 11 21 syl121anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑋 ∈ 𝑉 )
24 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑋 ) )
25 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
26 25 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) )
27 24 26 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ↔ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
28 27 rspcv ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) → ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
29 23 28 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) → ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
30 12 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) )
33 31 32 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) = ( 𝐺 ‘ 𝑋 ) )
34 33 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) )
35 2 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝑆 ∈ DivRing )
36 7 35 syl ⊢ ( 𝜑 → 𝑆 ∈ DivRing )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑆 ∈ DivRing )
38 2 3 1 5 lflcl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 )
39 7 9 8 38 syl3anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 )
41 13 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
42 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
43 eqid ⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
44 3 4 20 42 43 drnginvrl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) = ( 1r ‘ 𝑆 ) )
45 37 40 41 44 syl3anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) = ( 1r ‘ 𝑆 ) )
46 45 oveq1d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) 𝑟 ) = ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑟 ) )
47 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
48 7 47 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
49 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ Ring )
50 48 49 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑆 ∈ Ring )
52 3 4 43 drnginvrcl ⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑅 )
53 37 40 41 52 syl3anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑅 )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → 𝑟 ∈ 𝑅 )
55 3 20 ringass ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝑅 ∧ 𝑟 ∈ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) 𝑟 ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
56 51 53 40 54 55 syl13anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) 𝑟 ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
57 3 20 42 ringlidm ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑟 ∈ 𝑅 ) → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑟 ) = 𝑟 )
58 51 54 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( 1r ‘ 𝑆 ) ( .r ‘ 𝑆 ) 𝑟 ) = 𝑟 )
59 46 56 58 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) = 𝑟 )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) = 𝑟 )
61 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐺 ‘ 𝑋 ) ) ( .r ‘ 𝑆 ) ( 𝐺 ‘ 𝑋 ) ) = ( 1r ‘ 𝑆 ) )
62 34 60 61 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) ∧ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) ) → 𝑟 = ( 1r ‘ 𝑆 ) )
63 62 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝐻 ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ 𝑆 ) 𝑟 ) → 𝑟 = ( 1r ‘ 𝑆 ) ) )
64 29 63 syld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) → 𝑟 = ( 1r ‘ 𝑆 ) ) )
65 64 ancrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑅 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) → ( 𝑟 = ( 1r ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ) ) )
66 65 reximdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) → ∃ 𝑟 ∈ 𝑅 ( 𝑟 = ( 1r ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ) ) )
67 22 66 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑅 ( 𝑟 = ( 1r ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ) )
68 3 42 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ 𝑅 )
69 50 68 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ 𝑅 )
70 oveq2 ⊢ ( 𝑟 = ( 1r ‘ 𝑆 ) → ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
71 70 eqeq2d ⊢ ( 𝑟 = ( 1r ‘ 𝑆 ) → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ↔ ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
72 71 ralbidv ⊢ ( 𝑟 = ( 1r ‘ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
73 72 ceqsrexv ⊢ ( ( 1r ‘ 𝑆 ) ∈ 𝑅 → ( ∃ 𝑟 ∈ 𝑅 ( 𝑟 = ( 1r ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
74 69 73 syl ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑅 ( 𝑟 = ( 1r ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) 𝑟 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
75 67 74 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
76 75 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
77 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ LMod )
78 77 49 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑆 ∈ Ring )
79 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ LVec )
80 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝐺 ∈ 𝐹 )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
82 2 3 1 5 lflcl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑅 )
83 79 80 81 82 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑅 )
84 3 20 42 ringridm ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑅 ) → ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( 𝐺 ‘ 𝑥 ) )
85 78 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐺 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( 𝐺 ‘ 𝑥 ) )
86 76 85 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
87 16 19 86 eqfnfvd ⊢ ( 𝜑 → 𝐺 = 𝐻 )