Step |
Hyp |
Ref |
Expression |
1 |
|
fveq1 |
โข ( ๐ = if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ด ยทโ ๐ต ) ) ) |
2 |
|
fveq1 |
โข ( ๐ = if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ โ ๐ต ) = ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ๐ต ) ) |
3 |
2
|
oveq2d |
โข ( ๐ = if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ด ยท ( ๐ โ ๐ต ) ) = ( ๐ด ยท ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ๐ต ) ) ) |
4 |
1 3
|
eqeq12d |
โข ( ๐ = if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( ๐ โ ๐ต ) ) โ ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ๐ต ) ) ) ) |
5 |
4
|
imbi2d |
โข ( ๐ = if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( ๐ โ ๐ต ) ) ) โ ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ๐ต ) ) ) ) ) |
6 |
|
0lnfn |
โข ( โ ร { 0 } ) โ LinFn |
7 |
6
|
elimel |
โข if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ LinFn |
8 |
7
|
lnfnmuli |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( if ( ๐ โ LinFn , ๐ , ( โ ร { 0 } ) ) โ ๐ต ) ) ) |
9 |
5 8
|
dedth |
โข ( ๐ โ LinFn โ ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( ๐ โ ๐ต ) ) ) ) |
10 |
9
|
3impib |
โข ( ( ๐ โ LinFn โง ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ โ ( ๐ด ยทโ ๐ต ) ) = ( ๐ด ยท ( ๐ โ ๐ต ) ) ) |