MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmphl Structured version   Visualization version   GIF version

Theorem frlmphl 21801
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.)
Hypotheses
Ref Expression
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
Ref Expression
frlmphl (𝜑𝑌 ∈ PreHil)
Distinct variable groups:   𝐵,𝑔,𝑥   𝑔,𝐼,𝑥   𝑅,𝑔,𝑥   𝑔,𝑉,𝑥   𝑔,𝑊,𝑥   · ,𝑔,𝑥   𝑔,𝑌,𝑥   0 ,𝑔,𝑥   𝜑,𝑔,𝑥   , ,𝑔,𝑥   𝑔,𝑂   𝑥,
Allowed substitution hints:   (𝑔)   𝑂(𝑥)

Proof of Theorem frlmphl
Dummy variables 𝑓 𝑒 𝑖 𝑦 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmphl.v . . 3 𝑉 = (Base‘𝑌)
21a1i 11 . 2 (𝜑𝑉 = (Base‘𝑌))
3 eqidd 2738 . 2 (𝜑 → (+g𝑌) = (+g𝑌))
4 eqidd 2738 . 2 (𝜑 → ( ·𝑠𝑌) = ( ·𝑠𝑌))
5 frlmphl.j . . 3 , = (·𝑖𝑌)
65a1i 11 . 2 (𝜑, = (·𝑖𝑌))
7 frlmphl.o . . 3 𝑂 = (0g𝑌)
87a1i 11 . 2 (𝜑𝑂 = (0g𝑌))
9 frlmphl.f . . . . 5 (𝜑𝑅 ∈ Field)
10 isfld 20740 . . . . 5 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
119, 10sylib 218 . . . 4 (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
1211simpld 494 . . 3 (𝜑𝑅 ∈ DivRing)
13 frlmphl.i . . 3 (𝜑𝐼𝑊)
14 frlmphl.y . . . 4 𝑌 = (𝑅 freeLMod 𝐼)
1514frlmsca 21773 . . 3 ((𝑅 ∈ DivRing ∧ 𝐼𝑊) → 𝑅 = (Scalar‘𝑌))
1612, 13, 15syl2anc 584 . 2 (𝜑𝑅 = (Scalar‘𝑌))
17 frlmphl.b . . 3 𝐵 = (Base‘𝑅)
1817a1i 11 . 2 (𝜑𝐵 = (Base‘𝑅))
19 eqidd 2738 . 2 (𝜑 → (+g𝑅) = (+g𝑅))
20 frlmphl.t . . 3 · = (.r𝑅)
2120a1i 11 . 2 (𝜑· = (.r𝑅))
22 frlmphl.s . . 3 = (*𝑟𝑅)
2322a1i 11 . 2 (𝜑 = (*𝑟𝑅))
24 frlmphl.0 . . 3 0 = (0g𝑅)
2524a1i 11 . 2 (𝜑0 = (0g𝑅))
2612drngringd 20737 . . . 4 (𝜑𝑅 ∈ Ring)
2714frlmlmod 21769 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼𝑊) → 𝑌 ∈ LMod)
2826, 13, 27syl2anc 584 . . 3 (𝜑𝑌 ∈ LMod)
2916, 12eqeltrrd 2842 . . 3 (𝜑 → (Scalar‘𝑌) ∈ DivRing)
30 eqid 2737 . . . 4 (Scalar‘𝑌) = (Scalar‘𝑌)
3130islvec 21103 . . 3 (𝑌 ∈ LVec ↔ (𝑌 ∈ LMod ∧ (Scalar‘𝑌) ∈ DivRing))
3228, 29, 31sylanbrc 583 . 2 (𝜑𝑌 ∈ LVec)
339fldcrngd 20742 . . 3 (𝜑𝑅 ∈ CRing)
34 frlmphl.u . . 3 ((𝜑𝑥𝐵) → ( 𝑥) = 𝑥)
3517, 22, 33, 34idsrngd 20857 . 2 (𝜑𝑅 ∈ *-Ring)
36133ad2ant1 1134 . . . . 5 ((𝜑𝑔𝑉𝑉) → 𝐼𝑊)
37263ad2ant1 1134 . . . . 5 ((𝜑𝑔𝑉𝑉) → 𝑅 ∈ Ring)
38 simp2 1138 . . . . 5 ((𝜑𝑔𝑉𝑉) → 𝑔𝑉)
39 simp3 1139 . . . . 5 ((𝜑𝑔𝑉𝑉) → 𝑉)
4014, 17, 20, 1, 5frlmipval 21799 . . . . 5 (((𝐼𝑊𝑅 ∈ Ring) ∧ (𝑔𝑉𝑉)) → (𝑔 , ) = (𝑅 Σg (𝑔f · )))
4136, 37, 38, 39, 40syl22anc 839 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑔 , ) = (𝑅 Σg (𝑔f · )))
4214, 17, 1frlmbasmap 21779 . . . . . . . . 9 ((𝐼𝑊𝑔𝑉) → 𝑔 ∈ (𝐵m 𝐼))
4336, 38, 42syl2anc 584 . . . . . . . 8 ((𝜑𝑔𝑉𝑉) → 𝑔 ∈ (𝐵m 𝐼))
44 elmapi 8889 . . . . . . . 8 (𝑔 ∈ (𝐵m 𝐼) → 𝑔:𝐼𝐵)
4543, 44syl 17 . . . . . . 7 ((𝜑𝑔𝑉𝑉) → 𝑔:𝐼𝐵)
4645ffnd 6737 . . . . . 6 ((𝜑𝑔𝑉𝑉) → 𝑔 Fn 𝐼)
4714, 17, 1frlmbasmap 21779 . . . . . . . . 9 ((𝐼𝑊𝑉) → ∈ (𝐵m 𝐼))
4836, 39, 47syl2anc 584 . . . . . . . 8 ((𝜑𝑔𝑉𝑉) → ∈ (𝐵m 𝐼))
49 elmapi 8889 . . . . . . . 8 ( ∈ (𝐵m 𝐼) → :𝐼𝐵)
5048, 49syl 17 . . . . . . 7 ((𝜑𝑔𝑉𝑉) → :𝐼𝐵)
5150ffnd 6737 . . . . . 6 ((𝜑𝑔𝑉𝑉) → Fn 𝐼)
52 inidm 4227 . . . . . 6 (𝐼𝐼) = 𝐼
53 eqidd 2738 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → (𝑔𝑥) = (𝑔𝑥))
54 eqidd 2738 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → (𝑥) = (𝑥))
5546, 51, 36, 36, 52, 53, 54offval 7706 . . . . 5 ((𝜑𝑔𝑉𝑉) → (𝑔f · ) = (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))
5655oveq2d 7447 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑅 Σg (𝑔f · )) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
5741, 56eqtrd 2777 . . 3 ((𝜑𝑔𝑉𝑉) → (𝑔 , ) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
5826ringcmnd 20281 . . . . 5 (𝜑𝑅 ∈ CMnd)
59583ad2ant1 1134 . . . 4 ((𝜑𝑔𝑉𝑉) → 𝑅 ∈ CMnd)
6037adantr 480 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → 𝑅 ∈ Ring)
6145ffvelcdmda 7104 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝐵)
6250ffvelcdmda 7104 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → (𝑥) ∈ 𝐵)
6317, 20, 60, 61, 62ringcld 20257 . . . . 5 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → ((𝑔𝑥) · (𝑥)) ∈ 𝐵)
6463fmpttd 7135 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))):𝐼𝐵)
65 frlmphl.m . . . . 5 ((𝜑𝑔𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂)
6614, 17, 20, 1, 5, 7, 24, 22, 9, 65, 34, 13frlmphllem 21800 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))) finSupp 0 )
6717, 24, 59, 36, 64, 66gsumcl 19933 . . 3 ((𝜑𝑔𝑉𝑉) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))) ∈ 𝐵)
6857, 67eqeltrd 2841 . 2 ((𝜑𝑔𝑉𝑉) → (𝑔 , ) ∈ 𝐵)
69 eqid 2737 . . . 4 (+g𝑅) = (+g𝑅)
70583ad2ant1 1134 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑅 ∈ CMnd)
71133ad2ant1 1134 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝐼𝑊)
72263ad2ant1 1134 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑅 ∈ Ring)
7372adantr 480 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → 𝑅 ∈ Ring)
74 simp2 1138 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑘𝐵)
7574adantr 480 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → 𝑘𝐵)
76 simp31 1210 . . . . . . . . 9 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑔𝑉)
7771, 76, 42syl2anc 584 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑔 ∈ (𝐵m 𝐼))
7877, 44syl 17 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑔:𝐼𝐵)
7978ffvelcdmda 7104 . . . . . 6 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝐵)
80 simp33 1212 . . . . . . . . 9 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑖𝑉)
8114, 17, 1frlmbasmap 21779 . . . . . . . . 9 ((𝐼𝑊𝑖𝑉) → 𝑖 ∈ (𝐵m 𝐼))
8271, 80, 81syl2anc 584 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑖 ∈ (𝐵m 𝐼))
83 elmapi 8889 . . . . . . . 8 (𝑖 ∈ (𝐵m 𝐼) → 𝑖:𝐼𝐵)
8482, 83syl 17 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑖:𝐼𝐵)
8584ffvelcdmda 7104 . . . . . 6 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑖𝑥) ∈ 𝐵)
8617, 20, 73, 79, 85ringcld 20257 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑔𝑥) · (𝑖𝑥)) ∈ 𝐵)
8717, 20, 73, 75, 86ringcld 20257 . . . 4 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑘 · ((𝑔𝑥) · (𝑖𝑥))) ∈ 𝐵)
88 simp32 1211 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑉)
8971, 88, 47syl2anc 584 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ∈ (𝐵m 𝐼))
9089, 49syl 17 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → :𝐼𝐵)
9190ffvelcdmda 7104 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝐵)
9217, 20, 73, 91, 85ringcld 20257 . . . 4 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑥) · (𝑖𝑥)) ∈ 𝐵)
93 eqidd 2738 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))) = (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))
94 eqidd 2738 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))) = (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))))
95 fveq2 6906 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑔𝑥) = (𝑔𝑦))
9695oveq2d 7447 . . . . . . . 8 (𝑥 = 𝑦 → (𝑘 · (𝑔𝑥)) = (𝑘 · (𝑔𝑦)))
9796cbvmptv 5255 . . . . . . 7 (𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) = (𝑦𝐼 ↦ (𝑘 · (𝑔𝑦)))
9897oveq1i 7441 . . . . . 6 ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) = ((𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) ∘f · 𝑖)
9917, 20, 73, 75, 79ringcld 20257 . . . . . . . . . . 11 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑘 · (𝑔𝑥)) ∈ 𝐵)
10099fmpttd 7135 . . . . . . . . . 10 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))):𝐼𝐵)
101100ffnd 6737 . . . . . . . . 9 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) Fn 𝐼)
10297fneq1i 6665 . . . . . . . . 9 ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) Fn 𝐼 ↔ (𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) Fn 𝐼)
103101, 102sylib 218 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) Fn 𝐼)
10484ffnd 6737 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑖 Fn 𝐼)
105 eqidd 2738 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) = (𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))))
106 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
107106fveq2d 6910 . . . . . . . . . 10 ((((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) ∧ 𝑦 = 𝑥) → (𝑔𝑦) = (𝑔𝑥))
108107oveq2d 7447 . . . . . . . . 9 ((((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) ∧ 𝑦 = 𝑥) → (𝑘 · (𝑔𝑦)) = (𝑘 · (𝑔𝑥)))
109 simpr 484 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → 𝑥𝐼)
110 ovexd 7466 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑘 · (𝑔𝑥)) ∈ V)
111105, 108, 109, 110fvmptd 7023 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑦𝐼 ↦ (𝑘 · (𝑔𝑦)))‘𝑥) = (𝑘 · (𝑔𝑥)))
112 eqidd 2738 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑖𝑥) = (𝑖𝑥))
113103, 104, 71, 71, 52, 111, 112offval 7706 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) ∘f · 𝑖) = (𝑥𝐼 ↦ ((𝑘 · (𝑔𝑥)) · (𝑖𝑥))))
11417, 20ringass 20250 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ (𝑘𝐵 ∧ (𝑔𝑥) ∈ 𝐵 ∧ (𝑖𝑥) ∈ 𝐵)) → ((𝑘 · (𝑔𝑥)) · (𝑖𝑥)) = (𝑘 · ((𝑔𝑥) · (𝑖𝑥))))
11573, 75, 79, 85, 114syl13anc 1374 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑘 · (𝑔𝑥)) · (𝑖𝑥)) = (𝑘 · ((𝑔𝑥) · (𝑖𝑥))))
116115mpteq2dva 5242 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ ((𝑘 · (𝑔𝑥)) · (𝑖𝑥))) = (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))
117113, 116eqtrd 2777 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑦𝐼 ↦ (𝑘 · (𝑔𝑦))) ∘f · 𝑖) = (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))
11898, 117eqtrid 2789 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) = (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))
119 ovexd 7466 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) ∈ V)
120101, 104, 71, 71offun 7711 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → Fun ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖))
121 simp3 1139 . . . . . . . . 9 ((𝑔𝑉𝑉𝑖𝑉) → 𝑖𝑉)
12213, 121anim12i 613 . . . . . . . 8 ((𝜑 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝐼𝑊𝑖𝑉))
1231223adant2 1132 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝐼𝑊𝑖𝑉))
12414, 24, 1frlmbasfsupp 21778 . . . . . . 7 ((𝐼𝑊𝑖𝑉) → 𝑖 finSupp 0 )
125123, 124syl 17 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑖 finSupp 0 )
12617, 24ring0cl 20264 . . . . . . . 8 (𝑅 ∈ Ring → 0𝐵)
12772, 126syl 17 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 0𝐵)
12817, 20, 24ringrz 20291 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑦𝐵) → (𝑦 · 0 ) = 0 )
12972, 128sylan 580 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑦𝐵) → (𝑦 · 0 ) = 0 )
13071, 127, 100, 84, 129suppofss2d 8230 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))
131 fsuppsssupp 9421 . . . . . 6 (((((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) ∈ V ∧ Fun ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖)) ∧ (𝑖 finSupp 0 ∧ (((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))) → ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) finSupp 0 )
132119, 120, 125, 130, 131syl22anc 839 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑥𝐼 ↦ (𝑘 · (𝑔𝑥))) ∘f · 𝑖) finSupp 0 )
133118, 132eqbrtrrd 5167 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))) finSupp 0 )
134 simp1 1137 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝜑)
135 eleq1w 2824 . . . . . . . . 9 (𝑔 = → (𝑔𝑉𝑉))
136 id 22 . . . . . . . . . . 11 (𝑔 = 𝑔 = )
137136, 136oveq12d 7449 . . . . . . . . . 10 (𝑔 = → (𝑔 , 𝑔) = ( , ))
138137eqeq1d 2739 . . . . . . . . 9 (𝑔 = → ((𝑔 , 𝑔) = 0 ↔ ( , ) = 0 ))
139135, 1383anbi23d 1441 . . . . . . . 8 (𝑔 = → ((𝜑𝑔𝑉 ∧ (𝑔 , 𝑔) = 0 ) ↔ (𝜑𝑉 ∧ ( , ) = 0 )))
140 eqeq1 2741 . . . . . . . 8 (𝑔 = → (𝑔 = 𝑂 = 𝑂))
141139, 140imbi12d 344 . . . . . . 7 (𝑔 = → (((𝜑𝑔𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) ↔ ((𝜑𝑉 ∧ ( , ) = 0 ) → = 𝑂)))
142141, 65chvarvv 1998 . . . . . 6 ((𝜑𝑉 ∧ ( , ) = 0 ) → = 𝑂)
14314, 17, 20, 1, 5, 7, 24, 22, 9, 142, 34, 13frlmphllem 21800 . . . . 5 ((𝜑𝑉𝑖𝑉) → (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))) finSupp 0 )
144134, 88, 80, 143syl3anc 1373 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))) finSupp 0 )
14517, 24, 69, 70, 71, 87, 92, 93, 94, 133, 144gsummptfsadd 19942 . . 3 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥))))) = ((𝑅 Σg (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))(+g𝑅)(𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))))))
14614, 17, 20frlmip 21798 . . . . . . . . 9 ((𝐼𝑊𝑅 ∈ DivRing) → (𝑔 ∈ (𝐵m 𝐼), ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))) = (·𝑖𝑌))
14713, 12, 146syl2anc 584 . . . . . . . 8 (𝜑 → (𝑔 ∈ (𝐵m 𝐼), ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))) = (·𝑖𝑌))
1485, 147eqtr4id 2796 . . . . . . 7 (𝜑, = (𝑔 ∈ (𝐵m 𝐼), ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))))
149 fveq1 6905 . . . . . . . . . . 11 (𝑒 = 𝑔 → (𝑒𝑥) = (𝑔𝑥))
150149oveq1d 7446 . . . . . . . . . 10 (𝑒 = 𝑔 → ((𝑒𝑥) · (𝑓𝑥)) = ((𝑔𝑥) · (𝑓𝑥)))
151150mpteq2dv 5244 . . . . . . . . 9 (𝑒 = 𝑔 → (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑓𝑥))))
152151oveq2d 7447 . . . . . . . 8 (𝑒 = 𝑔 → (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑓𝑥)))))
153 fveq1 6905 . . . . . . . . . . 11 (𝑓 = → (𝑓𝑥) = (𝑥))
154153oveq2d 7447 . . . . . . . . . 10 (𝑓 = → ((𝑔𝑥) · (𝑓𝑥)) = ((𝑔𝑥) · (𝑥)))
155154mpteq2dv 5244 . . . . . . . . 9 (𝑓 = → (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))
156155oveq2d 7447 . . . . . . . 8 (𝑓 = → (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
157152, 156cbvmpov 7528 . . . . . . 7 (𝑒 ∈ (𝐵m 𝐼), 𝑓 ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))))) = (𝑔 ∈ (𝐵m 𝐼), ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
158148, 157eqtr4di 2795 . . . . . 6 (𝜑, = (𝑒 ∈ (𝐵m 𝐼), 𝑓 ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))))))
1591583ad2ant1 1134 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → , = (𝑒 ∈ (𝐵m 𝐼), 𝑓 ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))))))
160 simprl 771 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → 𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)))
161160fveq1d 6908 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → (𝑒𝑥) = (((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥))
162 simprr 773 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖)
163162fveq1d 6908 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → (𝑓𝑥) = (𝑖𝑥))
164161, 163oveq12d 7449 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → ((𝑒𝑥) · (𝑓𝑥)) = ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)))
165164mpteq2dv 5244 . . . . . 6 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥))))
166165oveq2d 7447 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)))))
167283ad2ant1 1134 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑌 ∈ LMod)
168163ad2ant1 1134 . . . . . . . . . . 11 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑅 = (Scalar‘𝑌))
169168fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
17017, 169eqtrid 2789 . . . . . . . . 9 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝐵 = (Base‘(Scalar‘𝑌)))
17174, 170eleqtrd 2843 . . . . . . . 8 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → 𝑘 ∈ (Base‘(Scalar‘𝑌)))
172 eqid 2737 . . . . . . . . 9 ( ·𝑠𝑌) = ( ·𝑠𝑌)
173 eqid 2737 . . . . . . . . 9 (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
1741, 30, 172, 173lmodvscl 20876 . . . . . . . 8 ((𝑌 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑔𝑉) → (𝑘( ·𝑠𝑌)𝑔) ∈ 𝑉)
175167, 171, 76, 174syl3anc 1373 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑘( ·𝑠𝑌)𝑔) ∈ 𝑉)
176 eqid 2737 . . . . . . . 8 (+g𝑌) = (+g𝑌)
1771, 176lmodvacl 20873 . . . . . . 7 ((𝑌 ∈ LMod ∧ (𝑘( ·𝑠𝑌)𝑔) ∈ 𝑉𝑉) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∈ 𝑉)
178167, 175, 88, 177syl3anc 1373 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∈ 𝑉)
17914, 17, 1frlmbasmap 21779 . . . . . 6 ((𝐼𝑊 ∧ ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∈ 𝑉) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∈ (𝐵m 𝐼))
18071, 178, 179syl2anc 584 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) ∈ (𝐵m 𝐼))
181 ovexd 7466 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)))) ∈ V)
182159, 166, 180, 82, 181ovmpod 7585 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) , 𝑖) = (𝑅 Σg (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)))))
18314, 1, 72, 71, 175, 88, 69, 176frlmplusgval 21784 . . . . . . . . . 10 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) = ((𝑘( ·𝑠𝑌)𝑔) ∘f (+g𝑅)))
18414, 17, 1frlmbasmap 21779 . . . . . . . . . . . . 13 ((𝐼𝑊 ∧ (𝑘( ·𝑠𝑌)𝑔) ∈ 𝑉) → (𝑘( ·𝑠𝑌)𝑔) ∈ (𝐵m 𝐼))
18571, 175, 184syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑘( ·𝑠𝑌)𝑔) ∈ (𝐵m 𝐼))
186 elmapi 8889 . . . . . . . . . . . 12 ((𝑘( ·𝑠𝑌)𝑔) ∈ (𝐵m 𝐼) → (𝑘( ·𝑠𝑌)𝑔):𝐼𝐵)
187 ffn 6736 . . . . . . . . . . . 12 ((𝑘( ·𝑠𝑌)𝑔):𝐼𝐵 → (𝑘( ·𝑠𝑌)𝑔) Fn 𝐼)
188185, 186, 1873syl 18 . . . . . . . . . . 11 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑘( ·𝑠𝑌)𝑔) Fn 𝐼)
18990ffnd 6737 . . . . . . . . . . 11 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → Fn 𝐼)
19071adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → 𝐼𝑊)
19176adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → 𝑔𝑉)
19214, 1, 17, 190, 75, 191, 109, 172, 20frlmvscaval 21788 . . . . . . . . . . 11 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑘( ·𝑠𝑌)𝑔)‘𝑥) = (𝑘 · (𝑔𝑥)))
193 eqidd 2738 . . . . . . . . . . 11 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (𝑥) = (𝑥))
194188, 189, 71, 71, 52, 192, 193offval 7706 . . . . . . . . . 10 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘( ·𝑠𝑌)𝑔) ∘f (+g𝑅)) = (𝑥𝐼 ↦ ((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥))))
195183, 194eqtrd 2777 . . . . . . . . 9 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) = (𝑥𝐼 ↦ ((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥))))
196 ovexd 7466 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥)) ∈ V)
197195, 196fvmpt2d 7029 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) = ((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥)))
198197oveq1d 7446 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)) = (((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥)) · (𝑖𝑥)))
19917, 69, 20ringdir 20259 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ((𝑘 · (𝑔𝑥)) ∈ 𝐵 ∧ (𝑥) ∈ 𝐵 ∧ (𝑖𝑥) ∈ 𝐵)) → (((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥)) · (𝑖𝑥)) = (((𝑘 · (𝑔𝑥)) · (𝑖𝑥))(+g𝑅)((𝑥) · (𝑖𝑥))))
20073, 99, 91, 85, 199syl13anc 1374 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (((𝑘 · (𝑔𝑥))(+g𝑅)(𝑥)) · (𝑖𝑥)) = (((𝑘 · (𝑔𝑥)) · (𝑖𝑥))(+g𝑅)((𝑥) · (𝑖𝑥))))
201115oveq1d 7446 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → (((𝑘 · (𝑔𝑥)) · (𝑖𝑥))(+g𝑅)((𝑥) · (𝑖𝑥))) = ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥))))
202198, 200, 2013eqtrd 2781 . . . . . 6 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ 𝑥𝐼) → ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)) = ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥))))
203202mpteq2dva 5242 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥))) = (𝑥𝐼 ↦ ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥)))))
204203oveq2d 7447 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ ((((𝑘( ·𝑠𝑌)𝑔)(+g𝑌))‘𝑥) · (𝑖𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥))))))
205182, 204eqtrd 2777 . . 3 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) , 𝑖) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑘 · ((𝑔𝑥) · (𝑖𝑥)))(+g𝑅)((𝑥) · (𝑖𝑥))))))
206 simprl 771 . . . . . . . . . . 11 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → 𝑒 = 𝑔)
207206fveq1d 6908 . . . . . . . . . 10 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → (𝑒𝑥) = (𝑔𝑥))
208 simprr 773 . . . . . . . . . . 11 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → 𝑓 = 𝑖)
209208fveq1d 6908 . . . . . . . . . 10 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → (𝑓𝑥) = (𝑖𝑥))
210207, 209oveq12d 7449 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → ((𝑒𝑥) · (𝑓𝑥)) = ((𝑔𝑥) · (𝑖𝑥)))
211210mpteq2dv 5244 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥))))
212211oveq2d 7447 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑔𝑓 = 𝑖)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥)))))
213 ovexd 7466 . . . . . . 7 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥)))) ∈ V)
214159, 212, 77, 82, 213ovmpod 7585 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑔 , 𝑖) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥)))))
215214oveq2d 7447 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑘 · (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥))))))
21614, 17, 20, 1, 5, 7, 24, 22, 9, 65, 34, 13frlmphllem 21800 . . . . . . 7 ((𝜑𝑔𝑉𝑖𝑉) → (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥))) finSupp 0 )
217134, 76, 80, 216syl3anc 1373 . . . . . 6 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥))) finSupp 0 )
21817, 24, 20, 72, 71, 74, 86, 217gsummulc2 20314 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥))))) = (𝑘 · (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑖𝑥))))))
219215, 218eqtr4d 2780 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑅 Σg (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥))))))
220 simprl 771 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → 𝑒 = )
221220fveq1d 6908 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → (𝑒𝑥) = (𝑥))
222 simprr 773 . . . . . . . . 9 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → 𝑓 = 𝑖)
223222fveq1d 6908 . . . . . . . 8 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → (𝑓𝑥) = (𝑖𝑥))
224221, 223oveq12d 7449 . . . . . . 7 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → ((𝑒𝑥) · (𝑓𝑥)) = ((𝑥) · (𝑖𝑥)))
225224mpteq2dv 5244 . . . . . 6 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))))
226225oveq2d 7447 . . . . 5 (((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) ∧ (𝑒 = 𝑓 = 𝑖)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥)))))
227 ovexd 7466 . . . . 5 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥)))) ∈ V)
228159, 226, 89, 82, 227ovmpod 7585 . . . 4 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ( , 𝑖) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥)))))
229219, 228oveq12d 7449 . . 3 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → ((𝑘 · (𝑔 , 𝑖))(+g𝑅)( , 𝑖)) = ((𝑅 Σg (𝑥𝐼 ↦ (𝑘 · ((𝑔𝑥) · (𝑖𝑥)))))(+g𝑅)(𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑖𝑥))))))
230145, 205, 2293eqtr4d 2787 . 2 ((𝜑𝑘𝐵 ∧ (𝑔𝑉𝑉𝑖𝑉)) → (((𝑘( ·𝑠𝑌)𝑔)(+g𝑌)) , 𝑖) = ((𝑘 · (𝑔 , 𝑖))(+g𝑅)( , 𝑖)))
231333ad2ant1 1134 . . . . . . 7 ((𝜑𝑔𝑉𝑉) → 𝑅 ∈ CRing)
232231adantr 480 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → 𝑅 ∈ CRing)
23317, 20crngcom 20248 . . . . . 6 ((𝑅 ∈ CRing ∧ (𝑥) ∈ 𝐵 ∧ (𝑔𝑥) ∈ 𝐵) → ((𝑥) · (𝑔𝑥)) = ((𝑔𝑥) · (𝑥)))
234232, 62, 61, 233syl3anc 1373 . . . . 5 (((𝜑𝑔𝑉𝑉) ∧ 𝑥𝐼) → ((𝑥) · (𝑔𝑥)) = ((𝑔𝑥) · (𝑥)))
235234mpteq2dva 5242 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥))))
236235oveq2d 7447 . . 3 ((𝜑𝑔𝑉𝑉) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
2371583ad2ant1 1134 . . . 4 ((𝜑𝑔𝑉𝑉) → , = (𝑒 ∈ (𝐵m 𝐼), 𝑓 ∈ (𝐵m 𝐼) ↦ (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))))))
238 simprl 771 . . . . . . . 8 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → 𝑒 = )
239238fveq1d 6908 . . . . . . 7 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → (𝑒𝑥) = (𝑥))
240 simprr 773 . . . . . . . 8 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → 𝑓 = 𝑔)
241240fveq1d 6908 . . . . . . 7 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → (𝑓𝑥) = (𝑔𝑥))
242239, 241oveq12d 7449 . . . . . 6 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → ((𝑒𝑥) · (𝑓𝑥)) = ((𝑥) · (𝑔𝑥)))
243242mpteq2dv 5244 . . . . 5 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥))))
244243oveq2d 7447 . . . 4 (((𝜑𝑔𝑉𝑉) ∧ (𝑒 = 𝑓 = 𝑔)) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑒𝑥) · (𝑓𝑥)))) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥)))))
245 ovexd 7466 . . . 4 ((𝜑𝑔𝑉𝑉) → (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥)))) ∈ V)
246237, 244, 48, 43, 245ovmpod 7585 . . 3 ((𝜑𝑔𝑉𝑉) → ( , 𝑔) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑥) · (𝑔𝑥)))))
247 fveq2 6906 . . . . . 6 (𝑥 = (𝑔 , ) → ( 𝑥) = ( ‘(𝑔 , )))
248 id 22 . . . . . 6 (𝑥 = (𝑔 , ) → 𝑥 = (𝑔 , ))
249247, 248eqeq12d 2753 . . . . 5 (𝑥 = (𝑔 , ) → (( 𝑥) = 𝑥 ↔ ( ‘(𝑔 , )) = (𝑔 , )))
25034ralrimiva 3146 . . . . . 6 (𝜑 → ∀𝑥𝐵 ( 𝑥) = 𝑥)
2512503ad2ant1 1134 . . . . 5 ((𝜑𝑔𝑉𝑉) → ∀𝑥𝐵 ( 𝑥) = 𝑥)
252249, 251, 68rspcdva 3623 . . . 4 ((𝜑𝑔𝑉𝑉) → ( ‘(𝑔 , )) = (𝑔 , ))
253252, 57eqtrd 2777 . . 3 ((𝜑𝑔𝑉𝑉) → ( ‘(𝑔 , )) = (𝑅 Σg (𝑥𝐼 ↦ ((𝑔𝑥) · (𝑥)))))
254236, 246, 2533eqtr4rd 2788 . 2 ((𝜑𝑔𝑉𝑉) → ( ‘(𝑔 , )) = ( , 𝑔))
2552, 3, 4, 6, 8, 16, 18, 19, 21, 23, 25, 32, 35, 68, 230, 65, 254isphld 21672 1 (𝜑𝑌 ∈ PreHil)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  wss 3951   class class class wbr 5143  cmpt 5225  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  f cof 7695   supp csupp 8185  m cmap 8866   finSupp cfsupp 9401  Basecbs 17247  +gcplusg 17297  .rcmulr 17298  *𝑟cstv 17299  Scalarcsca 17300   ·𝑠 cvsca 17301  ·𝑖cip 17302  0gc0g 17484   Σg cgsu 17485  CMndccmn 19798  Ringcrg 20230  CRingccrg 20231  DivRingcdr 20729  Fieldcfield 20730  LModclmod 20858  LVecclvec 21101  PreHilcphl 21642   freeLMod cfrlm 21766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-oppr 20334  df-rhm 20472  df-subrg 20570  df-drng 20731  df-field 20732  df-staf 20840  df-srng 20841  df-lmod 20860  df-lss 20930  df-lmhm 21021  df-lvec 21102  df-sra 21172  df-rgmod 21173  df-phl 21644  df-dsmm 21752  df-frlm 21767
This theorem is referenced by:  rrxcph  25426
  Copyright terms: Public domain W3C validator