Step | Hyp | Ref
| Expression |
1 | | mvmulfval.x |
. 2
โข ร =
(๐
maVecMul โจ๐, ๐โฉ) |
2 | | df-mvmul 21842 |
. . . 4
โข maVecMul
= (๐ โ V, ๐ โ V โฆ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))))) |
3 | 2 | a1i 11 |
. . 3
โข (๐ โ maVecMul = (๐ โ V, ๐ โ V โฆ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))))) |
4 | | fvex 6852 |
. . . . 5
โข
(1st โ๐) โ V |
5 | | fvex 6852 |
. . . . 5
โข
(2nd โ๐) โ V |
6 | | xpeq12 5656 |
. . . . . . 7
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ (๐ ร ๐) = ((1st โ๐) ร (2nd
โ๐))) |
7 | 6 | oveq2d 7367 |
. . . . . 6
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ ((Baseโ๐) โm (๐ ร ๐)) = ((Baseโ๐) โm ((1st
โ๐) ร
(2nd โ๐)))) |
8 | | oveq2 7359 |
. . . . . . 7
โข (๐ = (2nd โ๐) โ ((Baseโ๐) โm ๐) = ((Baseโ๐) โm
(2nd โ๐))) |
9 | 8 | adantl 482 |
. . . . . 6
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ ((Baseโ๐) โm ๐) = ((Baseโ๐) โm (2nd
โ๐))) |
10 | | simpl 483 |
. . . . . . 7
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ ๐ = (1st โ๐)) |
11 | | simpr 485 |
. . . . . . . . 9
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ ๐ = (2nd โ๐)) |
12 | 11 | mpteq1d 5198 |
. . . . . . . 8
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))) = (๐ โ (2nd โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))) |
13 | 12 | oveq2d 7367 |
. . . . . . 7
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))) = (๐ ฮฃg (๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))) |
14 | 10, 13 | mpteq12dv 5194 |
. . . . . 6
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))) = (๐ โ (1st โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) |
15 | 7, 9, 14 | mpoeq123dv 7426 |
. . . . 5
โข ((๐ = (1st โ๐) โง ๐ = (2nd โ๐)) โ (๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) = (๐ฅ โ ((Baseโ๐) โm ((1st
โ๐) ร
(2nd โ๐))), ๐ฆ โ ((Baseโ๐) โm (2nd
โ๐)) โฆ (๐ โ (1st
โ๐) โฆ (๐ ฮฃg
(๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))))) |
16 | 4, 5, 15 | csbie2 3895 |
. . . 4
โข
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) = (๐ฅ โ ((Baseโ๐) โm ((1st
โ๐) ร
(2nd โ๐))), ๐ฆ โ ((Baseโ๐) โm (2nd
โ๐)) โฆ (๐ โ (1st
โ๐) โฆ (๐ ฮฃg
(๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) |
17 | | simprl 769 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ ๐ = ๐
) |
18 | 17 | fveq2d 6843 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (Baseโ๐) = (Baseโ๐
)) |
19 | | mvmulfval.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (Baseโ๐) = ๐ต) |
21 | | fveq2 6839 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐โฉ โ (1st โ๐) = (1st
โโจ๐, ๐โฉ)) |
22 | 21 | ad2antll 727 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (1st โ๐) = (1st
โโจ๐, ๐โฉ)) |
23 | | mvmulfval.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
24 | | mvmulfval.n |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
25 | | op1stg 7925 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐ โ Fin) โ
(1st โโจ๐, ๐โฉ) = ๐) |
26 | 23, 24, 25 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (1st
โโจ๐, ๐โฉ) = ๐) |
27 | 26 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (1st
โโจ๐, ๐โฉ) = ๐) |
28 | 22, 27 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (1st โ๐) = ๐) |
29 | | fveq2 6839 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐โฉ โ (2nd โ๐) = (2nd
โโจ๐, ๐โฉ)) |
30 | 29 | ad2antll 727 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (2nd โ๐) = (2nd
โโจ๐, ๐โฉ)) |
31 | | op2ndg 7926 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐ โ Fin) โ
(2nd โโจ๐, ๐โฉ) = ๐) |
32 | 23, 24, 31 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (2nd
โโจ๐, ๐โฉ) = ๐) |
33 | 32 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (2nd
โโจ๐, ๐โฉ) = ๐) |
34 | 30, 33 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (2nd โ๐) = ๐) |
35 | 28, 34 | xpeq12d 5662 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ ((1st
โ๐) ร
(2nd โ๐))
= (๐ ร ๐)) |
36 | 20, 35 | oveq12d 7369 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ ((Baseโ๐) โm
((1st โ๐)
ร (2nd โ๐))) = (๐ต โm (๐ ร ๐))) |
37 | 20, 34 | oveq12d 7369 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ ((Baseโ๐) โm
(2nd โ๐))
= (๐ต โm
๐)) |
38 | | fveq2 6839 |
. . . . . . . . . . . 12
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ = ๐
โง ๐ = โจ๐, ๐โฉ) โ (.rโ๐) = (.rโ๐
)) |
40 | 39 | adantl 482 |
. . . . . . . . . 10
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (.rโ๐) = (.rโ๐
)) |
41 | | mvmulfval.t |
. . . . . . . . . 10
โข ยท =
(.rโ๐
) |
42 | 40, 41 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (.rโ๐) = ยท ) |
43 | 42 | oveqd 7368 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)) = ((๐๐ฅ๐) ยท (๐ฆโ๐))) |
44 | 34, 43 | mpteq12dv 5194 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (๐ โ (2nd โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))) = (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐)))) |
45 | 17, 44 | oveq12d 7369 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (๐ ฮฃg (๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))) |
46 | 28, 45 | mpteq12dv 5194 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (๐ โ (1st โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))) = (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐)))))) |
47 | 36, 37, 46 | mpoeq123dv 7426 |
. . . 4
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ (๐ฅ โ ((Baseโ๐) โm ((1st
โ๐) ร
(2nd โ๐))), ๐ฆ โ ((Baseโ๐) โm (2nd
โ๐)) โฆ (๐ โ (1st
โ๐) โฆ (๐ ฮฃg
(๐ โ (2nd
โ๐) โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))))) |
48 | 16, 47 | eqtrid 2789 |
. . 3
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐โฉ)) โ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐)))))) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))))) |
49 | | mvmulfval.r |
. . . 4
โข (๐ โ ๐
โ ๐) |
50 | 49 | elexd 3463 |
. . 3
โข (๐ โ ๐
โ V) |
51 | | opex 5419 |
. . . 4
โข
โจ๐, ๐โฉ โ V |
52 | 51 | a1i 11 |
. . 3
โข (๐ โ โจ๐, ๐โฉ โ V) |
53 | | ovex 7384 |
. . . . 5
โข (๐ต โm (๐ ร ๐)) โ V |
54 | | ovex 7384 |
. . . . 5
โข (๐ต โm ๐) โ V |
55 | 53, 54 | mpoex 8004 |
. . . 4
โข (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐)))))) โ V |
56 | 55 | a1i 11 |
. . 3
โข (๐ โ (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐)))))) โ V) |
57 | 3, 48, 50, 52, 56 | ovmpod 7501 |
. 2
โข (๐ โ (๐
maVecMul โจ๐, ๐โฉ) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))))) |
58 | 1, 57 | eqtrid 2789 |
1
โข (๐ โ ร = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))))) |