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