Step | Hyp | Ref
| Expression |
1 | | 2a1 28 |
. 2
โข (๐ โ ๐ท โ (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท))) |
2 | | simpl 484 |
. . . . . . . . 9
โข ((๐
โ ๐ โง ๐ โ ๐ธ) โ ๐
โ ๐) |
3 | 2 | adantl 483 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ๐
โ ๐) |
4 | | simpl1 1192 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ๐ โ Fin) |
5 | | simpl2 1193 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ๐ โ Fin) |
6 | 3, 4, 5 | 3jca 1129 |
. . . . . . 7
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ (๐
โ ๐ โง ๐ โ Fin โง ๐ โ Fin)) |
7 | 6 | adantl 483 |
. . . . . 6
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ (๐
โ ๐ โง ๐ โ Fin โง ๐ โ Fin)) |
8 | | mavmuldm.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
9 | | mavmuldm.c |
. . . . . . 7
โข ๐ถ = (๐ต โm (๐ ร ๐)) |
10 | | mavmuldm.d |
. . . . . . 7
โข ๐ท = (๐ต โm ๐) |
11 | | mavmuldm.t |
. . . . . . 7
โข ยท =
(๐
maVecMul โจ๐, ๐โฉ) |
12 | 8, 9, 10, 11 | mavmuldm 21922 |
. . . . . 6
โข ((๐
โ ๐ โง ๐ โ Fin โง ๐ โ Fin) โ dom ยท = (๐ถ ร ๐ท)) |
13 | 7, 12 | syl 17 |
. . . . 5
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ dom ยท = (๐ถ ร ๐ท)) |
14 | | simpl 484 |
. . . . . 6
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ยฌ ๐ โ ๐ท) |
15 | 14 | intnand 490 |
. . . . 5
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ยฌ (๐ด โ ๐ถ โง ๐ โ ๐ท)) |
16 | | ndmovg 7541 |
. . . . 5
โข ((dom
ยท
= (๐ถ ร ๐ท) โง ยฌ (๐ด โ ๐ถ โง ๐ โ ๐ท)) โ (๐ด ยท ๐) = โ
) |
17 | 13, 15, 16 | syl2anc 585 |
. . . 4
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ (๐ด ยท ๐) = โ
) |
18 | | eqeq1 2737 |
. . . . . 6
โข ((๐ด ยท ๐) = โ
โ ((๐ด ยท ๐) = ๐ โ โ
= ๐)) |
19 | | elmapi 8793 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ต โm ๐) โ ๐:๐โถ๐ต) |
20 | | f0dom0 6730 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐:๐โถ๐ต โ (๐ = โ
โ ๐ = โ
)) |
21 | 20 | biimprd 248 |
. . . . . . . . . . . . . . . . . . 19
โข (๐:๐โถ๐ต โ (๐ = โ
โ ๐ = โ
)) |
22 | 21 | necon3d 2961 |
. . . . . . . . . . . . . . . . . 18
โข (๐:๐โถ๐ต โ (๐ โ โ
โ ๐ โ โ
)) |
23 | 22 | com12 32 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ
โ (๐:๐โถ๐ต โ ๐ โ โ
)) |
24 | 23 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ (๐:๐โถ๐ต โ ๐ โ โ
)) |
25 | 24 | com12 32 |
. . . . . . . . . . . . . . 15
โข (๐:๐โถ๐ต โ ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ ๐ โ โ
)) |
26 | 25 | a1d 25 |
. . . . . . . . . . . . . 14
โข (๐:๐โถ๐ต โ (๐
โ ๐ โ ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ ๐ โ โ
))) |
27 | 19, 26 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ต โm ๐) โ (๐
โ ๐ โ ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ ๐ โ โ
))) |
28 | | mavmulsolcl.e |
. . . . . . . . . . . . 13
โข ๐ธ = (๐ต โm ๐) |
29 | 27, 28 | eleq2s 2852 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ โ (๐
โ ๐ โ ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ ๐ โ โ
))) |
30 | 29 | impcom 409 |
. . . . . . . . . . 11
โข ((๐
โ ๐ โง ๐ โ ๐ธ) โ ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โ ๐ โ โ
)) |
31 | 30 | impcom 409 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ๐ โ โ
) |
32 | | eqneqall 2951 |
. . . . . . . . . 10
โข (๐ = โ
โ (๐ โ โ
โ ๐ โ ๐ท)) |
33 | 31, 32 | syl5com 31 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ (๐ = โ
โ ๐ โ ๐ท)) |
34 | 33 | adantl 483 |
. . . . . . . 8
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ (๐ = โ
โ ๐ โ ๐ท)) |
35 | 34 | com12 32 |
. . . . . . 7
โข (๐ = โ
โ ((ยฌ ๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ๐ โ ๐ท)) |
36 | 35 | eqcoms 2741 |
. . . . . 6
โข (โ
= ๐ โ ((ยฌ ๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ๐ โ ๐ท)) |
37 | 18, 36 | syl6bi 253 |
. . . . 5
โข ((๐ด ยท ๐) = โ
โ ((๐ด ยท ๐) = ๐ โ ((ยฌ ๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ๐ โ ๐ท))) |
38 | 37 | com23 86 |
. . . 4
โข ((๐ด ยท ๐) = โ
โ ((ยฌ ๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท))) |
39 | 17, 38 | mpcom 38 |
. . 3
โข ((ยฌ
๐ โ ๐ท โง ((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ))) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท)) |
40 | 39 | ex 414 |
. 2
โข (ยฌ
๐ โ ๐ท โ (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท))) |
41 | 1, 40 | pm2.61i 182 |
1
โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ
) โง (๐
โ ๐ โง ๐ โ ๐ธ)) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท)) |