Step |
Hyp |
Ref |
Expression |
1 |
|
pser.g |
โข ๐บ = ( ๐ฅ โ โ โฆ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) ) |
2 |
|
oveq1 |
โข ( ๐ฆ = ๐ โ ( ๐ฆ โ ๐ ) = ( ๐ โ ๐ ) ) |
3 |
2
|
oveq2d |
โข ( ๐ฆ = ๐ โ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) = ( ( ๐ด โ ๐ ) ยท ( ๐ โ ๐ ) ) ) |
4 |
3
|
mpteq2dv |
โข ( ๐ฆ = ๐ โ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ โ ๐ ) ) ) ) |
5 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ด โ ๐ ) = ( ๐ด โ ๐ ) ) |
6 |
|
oveq2 |
โข ( ๐ = ๐ โ ( ๐ฅ โ ๐ ) = ( ๐ฅ โ ๐ ) ) |
7 |
5 6
|
oveq12d |
โข ( ๐ = ๐ โ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) = ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) |
8 |
7
|
cbvmptv |
โข ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) |
9 |
|
oveq1 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ฅ โ ๐ ) = ( ๐ฆ โ ๐ ) ) |
10 |
9
|
oveq2d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) = ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) |
11 |
10
|
mpteq2dv |
โข ( ๐ฅ = ๐ฆ โ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) ) |
12 |
8 11
|
eqtrid |
โข ( ๐ฅ = ๐ฆ โ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) ) |
13 |
12
|
cbvmptv |
โข ( ๐ฅ โ โ โฆ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฅ โ ๐ ) ) ) ) = ( ๐ฆ โ โ โฆ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) ) |
14 |
1 13
|
eqtri |
โข ๐บ = ( ๐ฆ โ โ โฆ ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ฆ โ ๐ ) ) ) ) |
15 |
|
nn0ex |
โข โ0 โ V |
16 |
15
|
mptex |
โข ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ โ ๐ ) ) ) โ V |
17 |
4 14 16
|
fvmpt |
โข ( ๐ โ โ โ ( ๐บ โ ๐ ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) ยท ( ๐ โ ๐ ) ) ) ) |