Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7384 |
. . . . . 6
โข (๐ = 0 โ (๐นโ(๐ ยท ๐)) = (๐นโ(0 ยท ๐))) |
2 | | oveq1 7368 |
. . . . . 6
โข (๐ = 0 โ (๐ ร (๐นโ๐)) = (0 ร (๐นโ๐))) |
3 | 1, 2 | eqeq12d 2749 |
. . . . 5
โข (๐ = 0 โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ(0 ยท ๐)) = (0 ร (๐นโ๐)))) |
4 | 3 | imbi2d 341 |
. . . 4
โข (๐ = 0 โ (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(0 ยท ๐)) = (0 ร (๐นโ๐))))) |
5 | | fvoveq1 7384 |
. . . . . 6
โข (๐ = ๐ โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐))) |
6 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ โ (๐ ร (๐นโ๐)) = (๐ ร (๐นโ๐))) |
7 | 5, 6 | eqeq12d 2749 |
. . . . 5
โข (๐ = ๐ โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)))) |
8 | 7 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))))) |
9 | | fvoveq1 7384 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐นโ(๐ ยท ๐)) = (๐นโ((๐ + 1) ยท ๐))) |
10 | | oveq1 7368 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ ร (๐นโ๐)) = ((๐ + 1) ร (๐นโ๐))) |
11 | 9, 10 | eqeq12d 2749 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐)))) |
12 | 11 | imbi2d 341 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐))))) |
13 | | fvoveq1 7384 |
. . . . . 6
โข (๐ = ๐ โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐))) |
14 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ โ (๐ ร (๐นโ๐)) = (๐ ร (๐นโ๐))) |
15 | 13, 14 | eqeq12d 2749 |
. . . . 5
โข (๐ = ๐ โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)))) |
16 | 15 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))))) |
17 | | eqid 2733 |
. . . . . . 7
โข
(0gโ๐บ) = (0gโ๐บ) |
18 | | eqid 2733 |
. . . . . . 7
โข
(0gโ๐ป) = (0gโ๐ป) |
19 | 17, 18 | mhm0 18618 |
. . . . . 6
โข (๐น โ (๐บ MndHom ๐ป) โ (๐นโ(0gโ๐บ)) = (0gโ๐ป)) |
20 | 19 | adantr 482 |
. . . . 5
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(0gโ๐บ)) = (0gโ๐ป)) |
21 | | mhmmulg.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐บ) |
22 | | mhmmulg.s |
. . . . . . . 8
โข ยท =
(.gโ๐บ) |
23 | 21, 17, 22 | mulg0 18887 |
. . . . . . 7
โข (๐ โ ๐ต โ (0 ยท ๐) = (0gโ๐บ)) |
24 | 23 | adantl 483 |
. . . . . 6
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (0 ยท ๐) = (0gโ๐บ)) |
25 | 24 | fveq2d 6850 |
. . . . 5
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(0 ยท ๐)) = (๐นโ(0gโ๐บ))) |
26 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
27 | 21, 26 | mhmf 18615 |
. . . . . . 7
โข (๐น โ (๐บ MndHom ๐ป) โ ๐น:๐ตโถ(Baseโ๐ป)) |
28 | 27 | ffvelcdmda 7039 |
. . . . . 6
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ๐) โ (Baseโ๐ป)) |
29 | | mhmmulg.t |
. . . . . . 7
โข ร =
(.gโ๐ป) |
30 | 26, 18, 29 | mulg0 18887 |
. . . . . 6
โข ((๐นโ๐) โ (Baseโ๐ป) โ (0 ร (๐นโ๐)) = (0gโ๐ป)) |
31 | 28, 30 | syl 17 |
. . . . 5
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (0 ร (๐นโ๐)) = (0gโ๐ป)) |
32 | 20, 25, 31 | 3eqtr4d 2783 |
. . . 4
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(0 ยท ๐)) = (0 ร (๐นโ๐))) |
33 | | oveq1 7368 |
. . . . . . 7
โข ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ ((๐นโ(๐ ยท ๐))(+gโ๐ป)(๐นโ๐)) = ((๐ ร (๐นโ๐))(+gโ๐ป)(๐นโ๐))) |
34 | | mhmrcl1 18613 |
. . . . . . . . . . . 12
โข (๐น โ (๐บ MndHom ๐ป) โ ๐บ โ Mnd) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐บ โ Mnd) |
36 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ
โ0) |
37 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ ๐ต) |
38 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(+gโ๐บ) = (+gโ๐บ) |
39 | 21, 22, 38 | mulgnn0p1 18895 |
. . . . . . . . . . 11
โข ((๐บ โ Mnd โง ๐ โ โ0
โง ๐ โ ๐ต) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐)(+gโ๐บ)๐)) |
40 | 35, 36, 37, 39 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐)(+gโ๐บ)๐)) |
41 | 40 | fveq2d 6850 |
. . . . . . . . 9
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ((๐ + 1) ยท ๐)) = (๐นโ((๐ ยท ๐)(+gโ๐บ)๐))) |
42 | | simpll 766 |
. . . . . . . . . 10
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐น โ (๐บ MndHom ๐ป)) |
43 | 34 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐บ โ Mnd) |
44 | | simplr 768 |
. . . . . . . . . . . 12
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ โ0) |
45 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
46 | 21, 22, 43, 44, 45 | mulgnn0cld 18905 |
. . . . . . . . . . 11
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
47 | 46 | an32s 651 |
. . . . . . . . . 10
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐ ยท ๐) โ ๐ต) |
48 | | eqid 2733 |
. . . . . . . . . . 11
โข
(+gโ๐ป) = (+gโ๐ป) |
49 | 21, 38, 48 | mhmlin 18617 |
. . . . . . . . . 10
โข ((๐น โ (๐บ MndHom ๐ป) โง (๐ ยท ๐) โ ๐ต โง ๐ โ ๐ต) โ (๐นโ((๐ ยท ๐)(+gโ๐บ)๐)) = ((๐นโ(๐ ยท ๐))(+gโ๐ป)(๐นโ๐))) |
50 | 42, 47, 37, 49 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ((๐ ยท ๐)(+gโ๐บ)๐)) = ((๐นโ(๐ ยท ๐))(+gโ๐ป)(๐นโ๐))) |
51 | 41, 50 | eqtrd 2773 |
. . . . . . . 8
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐นโ(๐ ยท ๐))(+gโ๐ป)(๐นโ๐))) |
52 | | mhmrcl2 18614 |
. . . . . . . . . 10
โข (๐น โ (๐บ MndHom ๐ป) โ ๐ป โ Mnd) |
53 | 52 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ป โ Mnd) |
54 | 28 | adantr 482 |
. . . . . . . . 9
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐นโ๐) โ (Baseโ๐ป)) |
55 | 26, 29, 48 | mulgnn0p1 18895 |
. . . . . . . . 9
โข ((๐ป โ Mnd โง ๐ โ โ0
โง (๐นโ๐) โ (Baseโ๐ป)) โ ((๐ + 1) ร (๐นโ๐)) = ((๐ ร (๐นโ๐))(+gโ๐ป)(๐นโ๐))) |
56 | 53, 36, 54, 55 | syl3anc 1372 |
. . . . . . . 8
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐ + 1) ร (๐นโ๐)) = ((๐ ร (๐นโ๐))(+gโ๐ป)(๐นโ๐))) |
57 | 51, 56 | eqeq12d 2749 |
. . . . . . 7
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐)) โ ((๐นโ(๐ ยท ๐))(+gโ๐ป)(๐นโ๐)) = ((๐ ร (๐นโ๐))(+gโ๐ป)(๐นโ๐)))) |
58 | 33, 57 | syl5ibr 246 |
. . . . . 6
โข (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐)))) |
59 | 58 | expcom 415 |
. . . . 5
โข (๐ โ โ0
โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ ((๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐))))) |
60 | 59 | a2d 29 |
. . . 4
โข (๐ โ โ0
โ (((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ((๐ + 1) ยท ๐)) = ((๐ + 1) ร (๐นโ๐))))) |
61 | 4, 8, 12, 16, 32, 60 | nn0ind 12606 |
. . 3
โข (๐ โ โ0
โ ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐)))) |
62 | 61 | 3impib 1117 |
. 2
โข ((๐ โ โ0
โง ๐น โ (๐บ MndHom ๐ป) โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |
63 | 62 | 3com12 1124 |
1
โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) |