Step | Hyp | Ref
| Expression |
1 | | mnringmulrvald.1 |
. . . . 5
โข ๐น = (๐
MndRing ๐) |
2 | | mnringmulrvald.2 |
. . . . 5
โข ๐ต = (Baseโ๐น) |
3 | | mnringmulrvald.3 |
. . . . 5
โข โ =
(.rโ๐
) |
4 | | mnringmulrvald.4 |
. . . . 5
โข ๐ =
(0gโ๐
) |
5 | | mnringmulrvald.5 |
. . . . 5
โข ๐ด = (Baseโ๐) |
6 | | mnringmulrvald.6 |
. . . . 5
โข + =
(+gโ๐) |
7 | | mnringmulrvald.8 |
. . . . 5
โข (๐ โ ๐
โ ๐) |
8 | | mnringmulrvald.9 |
. . . . 5
โข (๐ โ ๐ โ ๐) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mnringmulrd 42593 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ ))))) =
(.rโ๐น)) |
10 | | mnringmulrvald.7 |
. . . 4
โข ยท =
(.rโ๐น) |
11 | 9, 10 | eqtr4di 2791 |
. . 3
โข (๐ โ (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ ))))) = ยท
) |
12 | 11 | eqcomd 2739 |
. 2
โข (๐ โ ยท = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐
)))))) |
13 | | fveq1 6845 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅโ๐) = (๐โ๐)) |
14 | | fveq1 6845 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (๐ฆโ๐) = (๐โ๐)) |
15 | 13, 14 | oveqan12d 7380 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ฅโ๐) โ (๐ฆโ๐)) = ((๐โ๐) โ (๐โ๐))) |
16 | 15 | ifeq1d 4509 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ ) = if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐ )) |
17 | 16 | mpteq2dv 5211 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ )) = (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐
))) |
18 | 17 | mpoeq3dv 7440 |
. . . 4
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ ))) = (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐
)))) |
19 | 18 | oveq2d 7377 |
. . 3
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ )))) = (๐น ฮฃg
(๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐
))))) |
20 | 19 | adantl 483 |
. 2
โข ((๐ โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐ฅโ๐) โ (๐ฆโ๐)), ๐ )))) = (๐น ฮฃg
(๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐
))))) |
21 | | mnringmulrvald.10 |
. 2
โข (๐ โ ๐ โ ๐ต) |
22 | | mnringmulrvald.11 |
. 2
โข (๐ โ ๐ โ ๐ต) |
23 | | ovexd 7396 |
. 2
โข (๐ โ (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐ )))) โ
V) |
24 | 12, 20, 21, 22, 23 | ovmpod 7511 |
1
โข (๐ โ (๐ ยท ๐) = (๐น ฮฃg (๐ โ ๐ด, ๐ โ ๐ด โฆ (๐ โ ๐ด โฆ if(๐ = (๐ + ๐), ((๐โ๐) โ (๐โ๐)), ๐
))))) |