Step | Hyp | Ref
| Expression |
1 | | mnringmulrd.1 |
. . . 4
β’ πΉ = (π
MndRing π) |
2 | | mnringmulrd.2 |
. . . 4
β’ π΅ = (BaseβπΉ) |
3 | | mnringmulrd.5 |
. . . 4
β’ π΄ = (Baseβπ) |
4 | | eqid 2737 |
. . . 4
β’ (π
freeLMod π΄) = (π
freeLMod π΄) |
5 | | mnringmulrd.7 |
. . . 4
β’ (π β π
β π) |
6 | | mnringmulrd.8 |
. . . 4
β’ (π β π β π) |
7 | 1, 2, 3, 4, 5, 6 | mnringbaserd 42404 |
. . 3
β’ (π β π΅ = (Baseβ(π
freeLMod π΄))) |
8 | 3 | fvexi 6853 |
. . . . . 6
β’ π΄ β V |
9 | 8, 8 | mpoex 8004 |
. . . . 5
β’ (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))) β
V |
10 | 9 | a1i 11 |
. . . 4
β’ (π β (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))) β
V) |
11 | 1 | ovexi 7385 |
. . . . 5
β’ πΉ β V |
12 | 11 | a1i 11 |
. . . 4
β’ (π β πΉ β V) |
13 | | ovex 7384 |
. . . . 5
β’ (π
freeLMod π΄) β V |
14 | 13 | a1i 11 |
. . . 4
β’ (π β (π
freeLMod π΄) β V) |
15 | 2, 7 | eqtr3id 2791 |
. . . 4
β’ (π β (BaseβπΉ) = (Baseβ(π
freeLMod π΄))) |
16 | 1, 3, 4, 5, 6 | mnringaddgd 42408 |
. . . . 5
β’ (π β
(+gβ(π
freeLMod π΄)) =
(+gβπΉ)) |
17 | 16 | eqcomd 2743 |
. . . 4
β’ (π β (+gβπΉ) = (+gβ(π
freeLMod π΄))) |
18 | 10, 12, 14, 15, 17 | gsumpropd 18493 |
. . 3
β’ (π β (πΉ Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 )))) = ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) |
19 | 7, 7, 18 | mpoeq123dv 7426 |
. 2
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (πΉ Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) = (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 )))))) |
20 | | fvex 6852 |
. . . . 5
β’
(Baseβ(π
freeLMod π΄)) β
V |
21 | 20, 20 | mpoex 8004 |
. . . 4
β’ (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) β
V |
22 | | mulrid 17135 |
. . . . 5
β’
.r = Slot (.rβndx) |
23 | 22 | setsid 17040 |
. . . 4
β’ (((π
freeLMod π΄) β V β§ (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) β V) β
(π₯ β
(Baseβ(π
freeLMod
π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) =
(.rβ((π
freeLMod π΄) sSet
β¨(.rβndx), (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0
)))))β©))) |
24 | 13, 21, 23 | mp2an 690 |
. . 3
β’ (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) =
(.rβ((π
freeLMod π΄) sSet
β¨(.rβndx), (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0
)))))β©)) |
25 | | mnringmulrd.3 |
. . . . 5
β’ Β· =
(.rβπ
) |
26 | | mnringmulrd.4 |
. . . . 5
β’ 0 =
(0gβπ
) |
27 | | mnringmulrd.6 |
. . . . 5
β’ + =
(+gβπ) |
28 | | eqid 2737 |
. . . . 5
β’
(Baseβ(π
freeLMod π΄)) =
(Baseβ(π
freeLMod
π΄)) |
29 | 1, 25, 26, 3, 27, 4, 28, 5, 6 | mnringvald 42399 |
. . . 4
β’ (π β πΉ = ((π
freeLMod π΄) sSet β¨(.rβndx),
(π₯ β
(Baseβ(π
freeLMod
π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0
)))))β©)) |
30 | 29 | fveq2d 6843 |
. . 3
β’ (π β (.rβπΉ) = (.rβ((π
freeLMod π΄) sSet β¨(.rβndx),
(π₯ β
(Baseβ(π
freeLMod
π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0
)))))β©))) |
31 | 24, 30 | eqtr4id 2796 |
. 2
β’ (π β (π₯ β (Baseβ(π
freeLMod π΄)), π¦ β (Baseβ(π
freeLMod π΄)) β¦ ((π
freeLMod π΄) Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) =
(.rβπΉ)) |
32 | 19, 31 | eqtrd 2777 |
1
β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (πΉ Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) =
(.rβπΉ)) |