Step | Hyp | Ref
| Expression |
1 | | oveq12 7370 |
. . 3
โข ((๐ = โ
โง ๐ = โ
) โ (๐ ยท ๐) = (โ
ยท
โ
)) |
2 | | mavmul0.t |
. . . 4
โข ยท =
(๐
maVecMul โจ๐, ๐โฉ) |
3 | 2 | mavmul0 21924 |
. . 3
โข ((๐ = โ
โง ๐
โ ๐) โ (โ
ยท โ
) =
โ
) |
4 | 1, 3 | sylan9eq 2793 |
. 2
โข (((๐ = โ
โง ๐ = โ
) โง (๐ = โ
โง ๐
โ ๐)) โ (๐ ยท ๐) = โ
) |
5 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ๐
) |
6 | | eqid 2733 |
. . . . . 6
โข
(.rโ๐
) = (.rโ๐
) |
7 | | simpr 486 |
. . . . . 6
โข ((๐ = โ
โง ๐
โ ๐) โ ๐
โ ๐) |
8 | | 0fin 9121 |
. . . . . . . 8
โข โ
โ Fin |
9 | | eleq1 2822 |
. . . . . . . 8
โข (๐ = โ
โ (๐ โ Fin โ โ
โ Fin)) |
10 | 8, 9 | mpbiri 258 |
. . . . . . 7
โข (๐ = โ
โ ๐ โ Fin) |
11 | 10 | adantr 482 |
. . . . . 6
โข ((๐ = โ
โง ๐
โ ๐) โ ๐ โ Fin) |
12 | 2, 5, 6, 7, 11, 11 | mvmulfval 21914 |
. . . . 5
โข ((๐ = โ
โง ๐
โ ๐) โ ยท = (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))))) |
13 | 12 | dmeqd 5865 |
. . . 4
โข ((๐ = โ
โง ๐
โ ๐) โ dom ยท = dom (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))))) |
14 | | 0ex 5268 |
. . . . . . . . . 10
โข โ
โ V |
15 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ = โ
โ (๐ โ V โ โ
โ
V)) |
16 | 14, 15 | mpbiri 258 |
. . . . . . . . 9
โข (๐ = โ
โ ๐ โ V) |
17 | 16 | mptexd 7178 |
. . . . . . . 8
โข (๐ = โ
โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) โ V) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ = โ
โง ๐
โ ๐) โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) โ V) |
19 | 18 | adantr 482 |
. . . . . 6
โข (((๐ = โ
โง ๐
โ ๐) โง (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โง ๐ โ ((Baseโ๐
) โm ๐))) โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) โ V) |
20 | 19 | ralrimivva 3194 |
. . . . 5
โข ((๐ = โ
โง ๐
โ ๐) โ โ๐ โ ((Baseโ๐
) โm (๐ ร ๐))โ๐ โ ((Baseโ๐
) โm ๐)(๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) โ V) |
21 | | eqid 2733 |
. . . . . 6
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) = (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
22 | 21 | dmmpoga 8009 |
. . . . 5
โข
(โ๐ โ
((Baseโ๐
)
โm (๐
ร ๐))โ๐ โ ((Baseโ๐
) โm ๐)(๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) โ V โ dom (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) = (((Baseโ๐
) โm (๐ ร ๐)) ร ((Baseโ๐
) โm ๐))) |
23 | 20, 22 | syl 17 |
. . . 4
โข ((๐ = โ
โง ๐
โ ๐) โ dom (๐ โ ((Baseโ๐
) โm (๐ ร ๐)), ๐ โ ((Baseโ๐
) โm ๐) โฆ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) = (((Baseโ๐
) โm (๐ ร ๐)) ร ((Baseโ๐
) โm ๐))) |
24 | | id 22 |
. . . . . . . . . . 11
โข (๐ = โ
โ ๐ = โ
) |
25 | 24, 24 | xpeq12d 5668 |
. . . . . . . . . 10
โข (๐ = โ
โ (๐ ร ๐) = (โ
ร
โ
)) |
26 | | 0xp 5734 |
. . . . . . . . . 10
โข (โ
ร โ
) = โ
|
27 | 25, 26 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ = โ
โ (๐ ร ๐) = โ
) |
28 | 27 | oveq2d 7377 |
. . . . . . . 8
โข (๐ = โ
โ
((Baseโ๐
)
โm (๐
ร ๐)) =
((Baseโ๐
)
โm โ
)) |
29 | | fvex 6859 |
. . . . . . . . 9
โข
(Baseโ๐
)
โ V |
30 | | map0e 8826 |
. . . . . . . . 9
โข
((Baseโ๐
)
โ V โ ((Baseโ๐
) โm โ
) =
1o) |
31 | 29, 30 | mp1i 13 |
. . . . . . . 8
โข (๐ = โ
โ
((Baseโ๐
)
โm โ
) = 1o) |
32 | 28, 31 | eqtrd 2773 |
. . . . . . 7
โข (๐ = โ
โ
((Baseโ๐
)
โm (๐
ร ๐)) =
1o) |
33 | 32 | adantr 482 |
. . . . . 6
โข ((๐ = โ
โง ๐
โ ๐) โ ((Baseโ๐
) โm (๐ ร ๐)) = 1o) |
34 | | df1o2 8423 |
. . . . . 6
โข
1o = {โ
} |
35 | 33, 34 | eqtrdi 2789 |
. . . . 5
โข ((๐ = โ
โง ๐
โ ๐) โ ((Baseโ๐
) โm (๐ ร ๐)) = {โ
}) |
36 | | oveq2 7369 |
. . . . . 6
โข (๐ = โ
โ
((Baseโ๐
)
โm ๐) =
((Baseโ๐
)
โm โ
)) |
37 | 29, 30 | mp1i 13 |
. . . . . . 7
โข (๐
โ ๐ โ ((Baseโ๐
) โm โ
) =
1o) |
38 | 37, 34 | eqtrdi 2789 |
. . . . . 6
โข (๐
โ ๐ โ ((Baseโ๐
) โm โ
) =
{โ
}) |
39 | 36, 38 | sylan9eq 2793 |
. . . . 5
โข ((๐ = โ
โง ๐
โ ๐) โ ((Baseโ๐
) โm ๐) = {โ
}) |
40 | 35, 39 | xpeq12d 5668 |
. . . 4
โข ((๐ = โ
โง ๐
โ ๐) โ (((Baseโ๐
) โm (๐ ร ๐)) ร ((Baseโ๐
) โm ๐)) = ({โ
} ร
{โ
})) |
41 | 13, 23, 40 | 3eqtrd 2777 |
. . 3
โข ((๐ = โ
โง ๐
โ ๐) โ dom ยท = ({โ
}
ร {โ
})) |
42 | | elsni 4607 |
. . . . 5
โข (๐ โ {โ
} โ ๐ = โ
) |
43 | | elsni 4607 |
. . . . 5
โข (๐ โ {โ
} โ ๐ = โ
) |
44 | 42, 43 | anim12i 614 |
. . . 4
โข ((๐ โ {โ
} โง ๐ โ {โ
}) โ (๐ = โ
โง ๐ = โ
)) |
45 | 44 | con3i 154 |
. . 3
โข (ยฌ
(๐ = โ
โง ๐ = โ
) โ ยฌ (๐ โ {โ
} โง ๐ โ
{โ
})) |
46 | | ndmovg 7541 |
. . 3
โข ((dom
ยท
= ({โ
} ร {โ
}) โง ยฌ (๐ โ {โ
} โง ๐ โ {โ
})) โ (๐ ยท ๐) = โ
) |
47 | 41, 45, 46 | syl2anr 598 |
. 2
โข ((ยฌ
(๐ = โ
โง ๐ = โ
) โง (๐ = โ
โง ๐
โ ๐)) โ (๐ ยท ๐) = โ
) |
48 | 4, 47 | pm2.61ian 811 |
1
โข ((๐ = โ
โง ๐
โ ๐) โ (๐ ยท ๐) = โ
) |