Step | Hyp | Ref
| Expression |
1 | | scmatval.s |
. 2
โข ๐ = (๐ ScMat ๐
) |
2 | | df-scmat 21863 |
. . . 4
โข ScMat =
(๐ โ Fin, ๐ โ V โฆ
โฆ(๐ Mat ๐) / ๐โฆ{๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))}) |
3 | 2 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ScMat = (๐ โ Fin, ๐ โ V โฆ โฆ(๐ Mat ๐) / ๐โฆ{๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))})) |
4 | | ovexd 7396 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ (๐ Mat ๐) โ V) |
5 | | fveq2 6846 |
. . . . . . 7
โข (๐ = (๐ Mat ๐) โ (Baseโ๐) = (Baseโ(๐ Mat ๐))) |
6 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ = (๐ Mat ๐) โ (
ยท๐ โ๐) = ( ยท๐
โ(๐ Mat ๐))) |
7 | | eqidd 2734 |
. . . . . . . . . 10
โข (๐ = (๐ Mat ๐) โ ๐ = ๐) |
8 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ = (๐ Mat ๐) โ (1rโ๐) = (1rโ(๐ Mat ๐))) |
9 | 6, 7, 8 | oveq123d 7382 |
. . . . . . . . 9
โข (๐ = (๐ Mat ๐) โ (๐( ยท๐
โ๐)(1rโ๐)) = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))) |
10 | 9 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ = (๐ Mat ๐) โ (๐ = (๐( ยท๐
โ๐)(1rโ๐)) โ ๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐))))) |
11 | 10 | rexbidv 3172 |
. . . . . . 7
โข (๐ = (๐ Mat ๐) โ (โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐)) โ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐))))) |
12 | 5, 11 | rabeqbidv 3423 |
. . . . . 6
โข (๐ = (๐ Mat ๐) โ {๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))} = {๐ โ (Baseโ(๐ Mat ๐)) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))}) |
13 | 12 | adantl 483 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โง ๐ = (๐ Mat ๐)) โ {๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))} = {๐ โ (Baseโ(๐ Mat ๐)) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))}) |
14 | 4, 13 | csbied 3897 |
. . . 4
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ โฆ(๐ Mat ๐) / ๐โฆ{๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))} = {๐ โ (Baseโ(๐ Mat ๐)) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))}) |
15 | | oveq12 7370 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat ๐) = (๐ Mat ๐
)) |
16 | 15 | fveq2d 6850 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat ๐)) = (Baseโ(๐ Mat ๐
))) |
17 | | scmatval.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐ด) |
18 | | scmatval.a |
. . . . . . . . 9
โข ๐ด = (๐ Mat ๐
) |
19 | 18 | fveq2i 6849 |
. . . . . . . 8
โข
(Baseโ๐ด) =
(Baseโ(๐ Mat ๐
)) |
20 | 17, 19 | eqtri 2761 |
. . . . . . 7
โข ๐ต = (Baseโ(๐ Mat ๐
)) |
21 | 16, 20 | eqtr4di 2791 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat ๐)) = ๐ต) |
22 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
23 | | scmatval.k |
. . . . . . . . 9
โข ๐พ = (Baseโ๐
) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ = ๐
โ (Baseโ๐) = ๐พ) |
25 | 24 | adantl 483 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ๐) = ๐พ) |
26 | 15 | fveq2d 6850 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(๐ Mat ๐)) = ( ยท๐
โ(๐ Mat ๐
))) |
27 | | scmatval.t |
. . . . . . . . . . 11
โข ยท = (
ยท๐ โ๐ด) |
28 | 18 | fveq2i 6849 |
. . . . . . . . . . 11
โข (
ยท๐ โ๐ด) = ( ยท๐
โ(๐ Mat ๐
)) |
29 | 27, 28 | eqtri 2761 |
. . . . . . . . . 10
โข ยท = (
ยท๐ โ(๐ Mat ๐
)) |
30 | 26, 29 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(๐ Mat ๐)) = ยท ) |
31 | | eqidd 2734 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ ๐ = ๐) |
32 | 15 | fveq2d 6850 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ (1rโ(๐ Mat ๐)) = (1rโ(๐ Mat ๐
))) |
33 | | scmatval.1 |
. . . . . . . . . . 11
โข 1 =
(1rโ๐ด) |
34 | 18 | fveq2i 6849 |
. . . . . . . . . . 11
โข
(1rโ๐ด) = (1rโ(๐ Mat ๐
)) |
35 | 33, 34 | eqtri 2761 |
. . . . . . . . . 10
โข 1 =
(1rโ(๐ Mat
๐
)) |
36 | 32, 35 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (1rโ(๐ Mat ๐)) = 1 ) |
37 | 30, 31, 36 | oveq123d 7382 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐))) = (๐ ยท 1 )) |
38 | 37 | eqeq2d 2744 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐))) โ ๐ = (๐ ยท 1 ))) |
39 | 25, 38 | rexeqbidv 3319 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐))) โ โ๐ โ ๐พ ๐ = (๐ ยท 1 ))) |
40 | 21, 39 | rabeqbidv 3423 |
. . . . 5
โข ((๐ = ๐ โง ๐ = ๐
) โ {๐ โ (Baseโ(๐ Mat ๐)) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))} = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )}) |
41 | 40 | adantl 483 |
. . . 4
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ {๐ โ (Baseโ(๐ Mat ๐)) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ(๐ Mat ๐))(1rโ(๐ Mat ๐)))} = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )}) |
42 | 14, 41 | eqtrd 2773 |
. . 3
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ โฆ(๐ Mat ๐) / ๐โฆ{๐ โ (Baseโ๐) โฃ โ๐ โ (Baseโ๐)๐ = (๐( ยท๐
โ๐)(1rโ๐))} = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )}) |
43 | | simpl 484 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ โ Fin) |
44 | | elex 3465 |
. . . 4
โข (๐
โ ๐ โ ๐
โ V) |
45 | 44 | adantl 483 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐
โ V) |
46 | 17 | fvexi 6860 |
. . . . 5
โข ๐ต โ V |
47 | 46 | rabex 5293 |
. . . 4
โข {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )} โ
V |
48 | 47 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )} โ
V) |
49 | 3, 42, 43, 45, 48 | ovmpod 7511 |
. 2
โข ((๐ โ Fin โง ๐
โ ๐) โ (๐ ScMat ๐
) = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )}) |
50 | 1, 49 | eqtrid 2785 |
1
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ = {๐ โ ๐ต โฃ โ๐ โ ๐พ ๐ = (๐ ยท 1 )}) |