Step |
Hyp |
Ref |
Expression |
1 |
|
hvmulcl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยทโ ๐ต ) โ โ ) |
2 |
|
brafval |
โข ( ( ๐ด ยทโ ๐ต ) โ โ โ ( bra โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ฅ โ โ โฆ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) ) ) |
3 |
1 2
|
syl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( bra โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ฅ โ โ โฆ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) ) ) |
4 |
|
cjcl |
โข ( ๐ด โ โ โ ( โ โ ๐ด ) โ โ ) |
5 |
|
brafn |
โข ( ๐ต โ โ โ ( bra โ ๐ต ) : โ โถ โ ) |
6 |
|
hfmmval |
โข ( ( ( โ โ ๐ด ) โ โ โง ( bra โ ๐ต ) : โ โถ โ ) โ ( ( โ โ ๐ด ) ยทfn ( bra โ ๐ต ) ) = ( ๐ฅ โ โ โฆ ( ( โ โ ๐ด ) ยท ( ( bra โ ๐ต ) โ ๐ฅ ) ) ) ) |
7 |
4 5 6
|
syl2an |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( โ โ ๐ด ) ยทfn ( bra โ ๐ต ) ) = ( ๐ฅ โ โ โฆ ( ( โ โ ๐ด ) ยท ( ( bra โ ๐ต ) โ ๐ฅ ) ) ) ) |
8 |
|
his5 |
โข ( ( ๐ด โ โ โง ๐ฅ โ โ โง ๐ต โ โ ) โ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) = ( ( โ โ ๐ด ) ยท ( ๐ฅ ยทih ๐ต ) ) ) |
9 |
8
|
3expa |
โข ( ( ( ๐ด โ โ โง ๐ฅ โ โ ) โง ๐ต โ โ ) โ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) = ( ( โ โ ๐ด ) ยท ( ๐ฅ ยทih ๐ต ) ) ) |
10 |
9
|
an32s |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ๐ฅ โ โ ) โ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) = ( ( โ โ ๐ด ) ยท ( ๐ฅ ยทih ๐ต ) ) ) |
11 |
|
braval |
โข ( ( ๐ต โ โ โง ๐ฅ โ โ ) โ ( ( bra โ ๐ต ) โ ๐ฅ ) = ( ๐ฅ ยทih ๐ต ) ) |
12 |
11
|
adantll |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ๐ฅ โ โ ) โ ( ( bra โ ๐ต ) โ ๐ฅ ) = ( ๐ฅ ยทih ๐ต ) ) |
13 |
12
|
oveq2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ๐ฅ โ โ ) โ ( ( โ โ ๐ด ) ยท ( ( bra โ ๐ต ) โ ๐ฅ ) ) = ( ( โ โ ๐ด ) ยท ( ๐ฅ ยทih ๐ต ) ) ) |
14 |
10 13
|
eqtr4d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ๐ฅ โ โ ) โ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) = ( ( โ โ ๐ด ) ยท ( ( bra โ ๐ต ) โ ๐ฅ ) ) ) |
15 |
14
|
mpteq2dva |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ฅ โ โ โฆ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) ) = ( ๐ฅ โ โ โฆ ( ( โ โ ๐ด ) ยท ( ( bra โ ๐ต ) โ ๐ฅ ) ) ) ) |
16 |
7 15
|
eqtr4d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( โ โ ๐ด ) ยทfn ( bra โ ๐ต ) ) = ( ๐ฅ โ โ โฆ ( ๐ฅ ยทih ( ๐ด ยทโ ๐ต ) ) ) ) |
17 |
3 16
|
eqtr4d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( bra โ ( ๐ด ยทโ ๐ต ) ) = ( ( โ โ ๐ด ) ยทfn ( bra โ ๐ต ) ) ) |