Metamath Proof Explorer

Theorem frlmphl

Description: Conditions for a free module to be a pre-Hilbert space. (Contributed by Thierry Arnoux, 21-Jun-2019) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmphl.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmphl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
frlmphl.t ⊢ · = ( .r ‘ 𝑅 )
frlmphl.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
frlmphl.j ⊢ , = ( ·𝑖 ‘ 𝑌 )
frlmphl.o ⊢ 𝑂 = ( 0g ‘ 𝑌 )
frlmphl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
frlmphl.s ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
frlmphl.f ⊢ ( 𝜑 → 𝑅 ∈ Field )
frlmphl.m ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) → 𝑔 = 𝑂 )
frlmphl.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
frlmphl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
Assertion frlmphl ( 𝜑 → 𝑌 ∈ PreHil )

Proof

Step Hyp Ref Expression
1 frlmphl.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmphl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 frlmphl.t ⊢ · = ( .r ‘ 𝑅 )
4 frlmphl.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
5 frlmphl.j ⊢ , = ( ·𝑖 ‘ 𝑌 )
6 frlmphl.o ⊢ 𝑂 = ( 0g ‘ 𝑌 )
7 frlmphl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
8 frlmphl.s ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
9 frlmphl.f ⊢ ( 𝜑 → 𝑅 ∈ Field )
10 frlmphl.m ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) → 𝑔 = 𝑂 )
11 frlmphl.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∗ ‘ 𝑥 ) = 𝑥 )
12 frlmphl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
13 4 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑌 ) )
14 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) )
15 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 ) )
16 5 a1i ⊢ ( 𝜑 → , = ( ·𝑖 ‘ 𝑌 ) )
17 6 a1i ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ 𝑌 ) )
18 isfld ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
19 9 18 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
20 19 simpld ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
21 1 frlmsca ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
22 20 12 21 syl2anc ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑌 ) )
23 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
24 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
25 3 a1i ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
26 8 a1i ⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝑅 ) )
27 7 a1i ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
28 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
29 20 28 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
30 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑌 ∈ LMod )
31 29 12 30 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ LMod )
32 22 20 eqeltrrd ⊢ ( 𝜑 → ( Scalar ‘ 𝑌 ) ∈ DivRing )
33 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
34 33 islvec ⊢ ( 𝑌 ∈ LVec ↔ ( 𝑌 ∈ LMod ∧ ( Scalar ‘ 𝑌 ) ∈ DivRing ) )
35 31 32 34 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ LVec )
36 19 simprd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
37 2 8 36 11 idsrngd ⊢ ( 𝜑 → 𝑅 ∈ *-Ring )
38 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝐼 ∈ 𝑊 )
39 29 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑅 ∈ Ring )
40 simp2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 ∈ 𝑉 )
41 simp3 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ 𝑉 )
42 1 2 3 4 5 frlmipval ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ) → ( 𝑔 , ℎ ) = ( 𝑅 Σg ( 𝑔 ∘f · ℎ ) ) )
43 38 39 40 41 42 syl22anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 , ℎ ) = ( 𝑅 Σg ( 𝑔 ∘f · ℎ ) ) )
44 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉 ) → 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) )
45 38 40 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) )
46 elmapi ⊢ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ 𝐵 )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 : 𝐼 ⟶ 𝐵 )
48 47 ffnd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑔 Fn 𝐼 )
49 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ ( 𝐵 ↑m 𝐼 ) )
50 38 41 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ ∈ ( 𝐵 ↑m 𝐼 ) )
51 elmapi ⊢ ( ℎ ∈ ( 𝐵 ↑m 𝐼 ) → ℎ : 𝐼 ⟶ 𝐵 )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ : 𝐼 ⟶ 𝐵 )
53 52 ffnd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ℎ Fn 𝐼 )
54 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
55 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
56 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
57 48 53 38 38 54 55 56 offval ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 ∘f · ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) )
58 57 oveq2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑅 Σg ( 𝑔 ∘f · ℎ ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
59 43 58 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 , ℎ ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
60 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
61 29 60 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
62 61 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑅 ∈ CMnd )
63 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
64 47 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
65 52 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) ∈ 𝐵 )
66 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ℎ ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ∈ 𝐵 )
67 63 64 65 66 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ∈ 𝐵 )
68 67 fmpttd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 )
69 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) finSupp 0 )
70 2 7 62 38 68 69 gsumcl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) ∈ 𝐵 )
71 59 70 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑔 , ℎ ) ∈ 𝐵 )
72 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
73 61 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑅 ∈ CMnd )
74 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑊 )
75 29 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑅 ∈ Ring )
76 75 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
77 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑘 ∈ 𝐵 )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑘 ∈ 𝐵 )
79 simp31 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑔 ∈ 𝑉 )
80 74 79 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) )
81 80 46 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑔 : 𝐼 ⟶ 𝐵 )
82 81 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
83 simp33 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑖 ∈ 𝑉 )
84 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉 ) → 𝑖 ∈ ( 𝐵 ↑m 𝐼 ) )
85 74 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑖 ∈ ( 𝐵 ↑m 𝐼 ) )
86 elmapi ⊢ ( 𝑖 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑖 : 𝐼 ⟶ 𝐵 )
87 85 86 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑖 : 𝐼 ⟶ 𝐵 )
88 87 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑖 ‘ 𝑥 ) ∈ 𝐵 )
89 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑖 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ∈ 𝐵 )
90 76 82 88 89 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ∈ 𝐵 )
91 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ∈ 𝐵 ) → ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ∈ 𝐵 )
92 76 78 90 91 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ∈ 𝐵 )
93 simp32 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ℎ ∈ 𝑉 )
94 74 93 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ℎ ∈ ( 𝐵 ↑m 𝐼 ) )
95 94 51 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ℎ : 𝐼 ⟶ 𝐵 )
96 95 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) ∈ 𝐵 )
97 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ℎ ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑖 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ∈ 𝐵 )
98 76 96 88 97 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ∈ 𝐵 )
99 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
100 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
101 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) )
102 101 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) = ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) )
103 102 cbvmptv ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) )
104 103 oveq1i ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) = ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) ∘f · 𝑖 )
105 2 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ∈ 𝐵 )
106 76 78 82 105 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ∈ 𝐵 )
107 106 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 )
108 107 ffnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) Fn 𝐼 )
109 103 fneq1i ⊢ ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) Fn 𝐼 ↔ ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) Fn 𝐼 )
110 108 109 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) Fn 𝐼 )
111 87 ffnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑖 Fn 𝐼 )
112 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) )
113 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
114 113 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 = 𝑥 ) → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑥 ) )
115 114 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 = 𝑥 ) → ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) = ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) )
116 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
117 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ∈ V )
118 112 115 116 117 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) )
119 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑖 ‘ 𝑥 ) = ( 𝑖 ‘ 𝑥 ) )
120 110 111 74 74 54 118 119 offval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) ∘f · 𝑖 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) ) )
121 2 3 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑖 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) = ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
122 76 78 82 88 121 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) = ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
123 122 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
124 120 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑦 ) ) ) ∘f · 𝑖 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
125 104 124 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
126 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) ∈ V )
127 funmpt ⊢ Fun ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑧 ) · ( 𝑖 ‘ 𝑧 ) ) )
128 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑧 ) )
129 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑖 ‘ 𝑧 ) = ( 𝑖 ‘ 𝑧 ) )
130 108 111 74 74 54 128 129 offval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑧 ) · ( 𝑖 ‘ 𝑧 ) ) ) )
131 130 funeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( Fun ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) ↔ Fun ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑧 ) · ( 𝑖 ‘ 𝑧 ) ) ) ) )
132 127 131 mpbiri ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → Fun ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) )
133 simp3 ⊢ ( ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) → 𝑖 ∈ 𝑉 )
134 12 133 anim12i ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉 ) )
135 134 3adant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉 ) )
136 1 7 4 frlmbasfsupp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉 ) → 𝑖 finSupp 0 )
137 135 136 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑖 finSupp 0 )
138 2 7 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
139 75 138 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 0 ∈ 𝐵 )
140 2 3 7 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 · 0 ) = 0 )
141 75 140 sylan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 · 0 ) = 0 )
142 74 139 107 87 141 suppofss2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) supp 0 ) ⊆ ( 𝑖 supp 0 ) )
143 fsuppsssupp ⊢ ( ( ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) ∈ V ∧ Fun ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) ) ∧ ( 𝑖 finSupp 0 ∧ ( ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) supp 0 ) ⊆ ( 𝑖 supp 0 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) finSupp 0 )
144 126 132 137 142 143 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ) ∘f · 𝑖 ) finSupp 0 )
145 125 144 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) finSupp 0 )
146 simp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝜑 )
147 eleq1w ⊢ ( 𝑔 = ℎ → ( 𝑔 ∈ 𝑉 ↔ ℎ ∈ 𝑉 ) )
148 id ⊢ ( 𝑔 = ℎ → 𝑔 = ℎ )
149 148 148 oveq12d ⊢ ( 𝑔 = ℎ → ( 𝑔 , 𝑔 ) = ( ℎ , ℎ ) )
150 149 eqeq1d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 , 𝑔 ) = 0 ↔ ( ℎ , ℎ ) = 0 ) )
151 147 150 3anbi23d ⊢ ( 𝑔 = ℎ → ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) ↔ ( 𝜑 ∧ ℎ ∈ 𝑉 ∧ ( ℎ , ℎ ) = 0 ) ) )
152 eqeq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 = 𝑂 ↔ ℎ = 𝑂 ) )
153 151 152 imbi12d ⊢ ( 𝑔 = ℎ → ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ( 𝑔 , 𝑔 ) = 0 ) → 𝑔 = 𝑂 ) ↔ ( ( 𝜑 ∧ ℎ ∈ 𝑉 ∧ ( ℎ , ℎ ) = 0 ) → ℎ = 𝑂 ) ) )
154 153 10 chvarvv ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑉 ∧ ( ℎ , ℎ ) = 0 ) → ℎ = 𝑂 )
155 1 2 3 4 5 6 7 8 9 154 11 12 frlmphllem ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) finSupp 0 )
156 146 93 83 155 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) finSupp 0 )
157 2 7 72 73 74 92 98 99 100 145 156 gsummptfsadd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
158 1 2 3 frlmip ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ DivRing ) → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) , ℎ ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )
159 12 20 158 syl2anc ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) , ℎ ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )
160 5 159 eqtr4id ⊢ ( 𝜑 → , = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) , ℎ ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) ) )
161 fveq1 ⊢ ( 𝑒 = 𝑔 → ( 𝑒 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
162 161 oveq1d ⊢ ( 𝑒 = 𝑔 → ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) )
163 162 mpteq2dv ⊢ ( 𝑒 = 𝑔 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) )
164 163 oveq2d ⊢ ( 𝑒 = 𝑔 → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) )
165 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
166 165 oveq2d ⊢ ( 𝑓 = ℎ → ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) )
167 166 mpteq2dv ⊢ ( 𝑓 = ℎ → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) )
168 167 oveq2d ⊢ ( 𝑓 = ℎ → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
169 164 168 cbvmpov ⊢ ( 𝑒 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) , ℎ ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
170 160 169 eqtr4di ⊢ ( 𝜑 → , = ( 𝑒 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
171 170 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → , = ( 𝑒 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
172 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) )
173 172 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → ( 𝑒 ‘ 𝑥 ) = ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) )
174 simprr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → 𝑓 = 𝑖 )
175 174 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑖 ‘ 𝑥 ) )
176 173 175 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) )
177 176 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
178 177 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∧ 𝑓 = 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
179 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑌 ∈ LMod )
180 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑅 = ( Scalar ‘ 𝑌 ) )
181 180 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
182 2 181 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
183 77 182 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
184 eqid ⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
185 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
186 4 33 184 185 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 𝑔 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ 𝑉 )
187 179 183 79 186 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ 𝑉 )
188 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
189 4 188 lmodvacl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∈ 𝑉 )
190 179 187 93 189 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∈ 𝑉 )
191 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∈ ( 𝐵 ↑m 𝐼 ) )
192 74 190 191 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ∈ ( 𝐵 ↑m 𝐼 ) )
193 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ∈ V )
194 171 178 192 85 193 ovmpod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) , 𝑖 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
195 1 4 75 74 187 93 72 188 frlmplusgval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∘f ( +g ‘ 𝑅 ) ℎ ) )
196 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ ( 𝐵 ↑m 𝐼 ) )
197 74 187 196 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ ( 𝐵 ↑m 𝐼 ) )
198 elmapi ⊢ ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∈ ( 𝐵 ↑m 𝐼 ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) : 𝐼 ⟶ 𝐵 )
199 ffn ⊢ ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) : 𝐼 ⟶ 𝐵 → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) Fn 𝐼 )
200 197 198 199 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) Fn 𝐼 )
201 95 ffnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ℎ Fn 𝐼 )
202 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
203 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑔 ∈ 𝑉 )
204 1 4 2 202 78 203 116 184 3 frlmvscaval ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ‘ 𝑥 ) = ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) )
205 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
206 200 201 74 74 54 204 205 offval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ∘f ( +g ‘ 𝑅 ) ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) ) )
207 195 206 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) ) )
208 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) ∈ V )
209 207 208 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) = ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) )
210 209 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) = ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) )
211 2 72 3 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ∈ 𝐵 ∧ ( ℎ ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑖 ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) = ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
212 76 106 96 88 211 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ℎ ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) = ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
213 122 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑘 · ( 𝑔 ‘ 𝑥 ) ) · ( 𝑖 ‘ 𝑥 ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) = ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
214 210 212 213 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) = ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
215 214 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
216 215 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
217 194 216 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) , 𝑖 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ( +g ‘ 𝑅 ) ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
218 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → 𝑒 = 𝑔 )
219 218 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → ( 𝑒 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
220 simprr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → 𝑓 = 𝑖 )
221 220 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑖 ‘ 𝑥 ) )
222 219 221 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) )
223 222 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
224 223 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = 𝑔 ∧ 𝑓 = 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
225 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ∈ V )
226 171 224 80 85 225 ovmpod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑔 , 𝑖 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
227 226 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑘 · ( 𝑔 , 𝑖 ) ) = ( 𝑘 · ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
228 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) finSupp 0 )
229 146 79 83 228 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) finSupp 0 )
230 2 7 72 3 75 74 77 90 229 gsummulc2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) = ( 𝑘 · ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
231 227 230 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑘 · ( 𝑔 , 𝑖 ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
232 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → 𝑒 = ℎ )
233 232 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → ( 𝑒 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
234 simprr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → 𝑓 = 𝑖 )
235 234 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑖 ‘ 𝑥 ) )
236 233 235 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) )
237 236 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) )
238 237 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑖 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
239 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ∈ V )
240 171 238 94 85 239 ovmpod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ℎ , 𝑖 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) )
241 231 240 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( 𝑘 · ( 𝑔 , 𝑖 ) ) ( +g ‘ 𝑅 ) ( ℎ , 𝑖 ) ) = ( ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( 𝑘 · ( ( 𝑔 ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) ( +g ‘ 𝑅 ) ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑖 ‘ 𝑥 ) ) ) ) ) )
242 157 217 241 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ∧ ( 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉 ) ) → ( ( ( 𝑘 ( ·𝑠 ‘ 𝑌 ) 𝑔 ) ( +g ‘ 𝑌 ) ℎ ) , 𝑖 ) = ( ( 𝑘 · ( 𝑔 , 𝑖 ) ) ( +g ‘ 𝑅 ) ( ℎ , 𝑖 ) ) )
243 36 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → 𝑅 ∈ CRing )
244 243 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CRing )
245 2 3 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( ℎ ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) )
246 244 65 64 245 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) )
247 246 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) )
248 247 oveq2d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
249 170 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → , = ( 𝑒 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
250 simprl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → 𝑒 = ℎ )
251 250 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → ( 𝑒 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
252 simprr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → 𝑓 = 𝑔 )
253 252 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
254 251 253 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) = ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) )
255 254 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) )
256 255 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) ∧ ( 𝑒 = ℎ ∧ 𝑓 = 𝑔 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑒 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) )
257 ovexd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ∈ V )
258 249 256 50 45 257 ovmpod ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ℎ , 𝑔 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) )
259 fveq2 ⊢ ( 𝑥 = ( 𝑔 , ℎ ) → ( ∗ ‘ 𝑥 ) = ( ∗ ‘ ( 𝑔 , ℎ ) ) )
260 id ⊢ ( 𝑥 = ( 𝑔 , ℎ ) → 𝑥 = ( 𝑔 , ℎ ) )
261 259 260 eqeq12d ⊢ ( 𝑥 = ( 𝑔 , ℎ ) → ( ( ∗ ‘ 𝑥 ) = 𝑥 ↔ ( ∗ ‘ ( 𝑔 , ℎ ) ) = ( 𝑔 , ℎ ) ) )
262 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ∗ ‘ 𝑥 ) = 𝑥 )
263 262 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝐵 ( ∗ ‘ 𝑥 ) = 𝑥 )
264 261 263 71 rspcdva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ∗ ‘ ( 𝑔 , ℎ ) ) = ( 𝑔 , ℎ ) )
265 264 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ∗ ‘ ( 𝑔 , ℎ ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑔 ‘ 𝑥 ) · ( ℎ ‘ 𝑥 ) ) ) ) )
266 248 258 265 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ) → ( ∗ ‘ ( 𝑔 , ℎ ) ) = ( ℎ , 𝑔 ) )
267 13 14 15 16 17 22 23 24 25 26 27 35 37 71 242 10 266 isphld ⊢ ( 𝜑 → 𝑌 ∈ PreHil )