Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
โข ( mulGrp โ ๐
) = ( mulGrp โ ๐
) |
2 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
3 |
1 2
|
mgpbas |
โข ( Base โ ๐
) = ( Base โ ( mulGrp โ ๐
) ) |
4 |
|
eqid |
โข ( .r โ ๐
) = ( .r โ ๐
) |
5 |
1 4
|
mgpplusg |
โข ( .r โ ๐
) = ( +g โ ( mulGrp โ ๐
) ) |
6 |
|
eqid |
โข ( +๐ โ ( mulGrp โ ๐
) ) = ( +๐ โ ( mulGrp โ ๐
) ) |
7 |
3 5 6
|
plusffval |
โข ( +๐ โ ( mulGrp โ ๐
) ) = ( ๐ฅ โ ( Base โ ๐
) , ๐ฆ โ ( Base โ ๐
) โฆ ( ๐ฅ ( .r โ ๐
) ๐ฆ ) ) |
8 |
|
rlmbas |
โข ( Base โ ๐
) = ( Base โ ( ringLMod โ ๐
) ) |
9 |
|
rlmsca2 |
โข ( I โ ๐
) = ( Scalar โ ( ringLMod โ ๐
) ) |
10 |
|
baseid |
โข Base = Slot ( Base โ ndx ) |
11 |
10 2
|
strfvi |
โข ( Base โ ๐
) = ( Base โ ( I โ ๐
) ) |
12 |
|
eqid |
โข ( ยทsf โ ( ringLMod โ ๐
) ) = ( ยทsf โ ( ringLMod โ ๐
) ) |
13 |
|
rlmvsca |
โข ( .r โ ๐
) = ( ยท๐ โ ( ringLMod โ ๐
) ) |
14 |
8 9 11 12 13
|
scaffval |
โข ( ยทsf โ ( ringLMod โ ๐
) ) = ( ๐ฅ โ ( Base โ ๐
) , ๐ฆ โ ( Base โ ๐
) โฆ ( ๐ฅ ( .r โ ๐
) ๐ฆ ) ) |
15 |
7 14
|
eqtr4i |
โข ( +๐ โ ( mulGrp โ ๐
) ) = ( ยทsf โ ( ringLMod โ ๐
) ) |