Step | Hyp | Ref
| Expression |
1 | | imassrn 6021 |
. . . 4
โข (๐ โ ๐ด) โ ran ๐ |
2 | | rnelsh.1 |
. . . . . 6
โข ๐ โ LinOp |
3 | 2 | lnopfi 30710 |
. . . . 5
โข ๐: โโถ
โ |
4 | | frn 6671 |
. . . . 5
โข (๐: โโถ โ โ
ran ๐ โ
โ) |
5 | 3, 4 | ax-mp 5 |
. . . 4
โข ran ๐ โ
โ |
6 | 1, 5 | sstri 3952 |
. . 3
โข (๐ โ ๐ด) โ โ |
7 | 2 | lnop0i 30711 |
. . . 4
โข (๐โ0โ) =
0โ |
8 | | imaelsh.2 |
. . . . . 6
โข ๐ด โ
Sโ |
9 | | sh0 29957 |
. . . . . 6
โข (๐ด โ
Sโ โ 0โ โ ๐ด) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
โข
0โ โ ๐ด |
11 | | ffun 6667 |
. . . . . . 7
โข (๐: โโถ โ โ
Fun ๐) |
12 | 3, 11 | ax-mp 5 |
. . . . . 6
โข Fun ๐ |
13 | 8 | shssii 29954 |
. . . . . . 7
โข ๐ด โ
โ |
14 | 3 | fdmi 6676 |
. . . . . . 7
โข dom ๐ = โ |
15 | 13, 14 | sseqtrri 3980 |
. . . . . 6
โข ๐ด โ dom ๐ |
16 | | funfvima2 7176 |
. . . . . 6
โข ((Fun
๐ โง ๐ด โ dom ๐) โ (0โ โ ๐ด โ (๐โ0โ) โ (๐ โ ๐ด))) |
17 | 12, 15, 16 | mp2an 691 |
. . . . 5
โข
(0โ โ ๐ด โ (๐โ0โ) โ (๐ โ ๐ด)) |
18 | 10, 17 | ax-mp 5 |
. . . 4
โข (๐โ0โ)
โ (๐ โ ๐ด) |
19 | 7, 18 | eqeltrri 2836 |
. . 3
โข
0โ โ (๐ โ ๐ด) |
20 | 6, 19 | pm3.2i 472 |
. 2
โข ((๐ โ ๐ด) โ โ โง 0โ
โ (๐ โ ๐ด)) |
21 | | ffn 6664 |
. . . . . 6
โข (๐: โโถ โ โ
๐ Fn
โ) |
22 | 3, 21 | ax-mp 5 |
. . . . 5
โข ๐ Fn โ |
23 | | oveq1 7357 |
. . . . . . . 8
โข (๐ข = (๐โ๐ฅ) โ (๐ข +โ ๐ฃ) = ((๐โ๐ฅ) +โ ๐ฃ)) |
24 | 23 | eleq1d 2823 |
. . . . . . 7
โข (๐ข = (๐โ๐ฅ) โ ((๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โ ((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด))) |
25 | 24 | ralbidv 3173 |
. . . . . 6
โข (๐ข = (๐โ๐ฅ) โ (โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฃ โ (๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด))) |
26 | 25 | ralima 7183 |
. . . . 5
โข ((๐ Fn โ โง ๐ด โ โ) โ
(โ๐ข โ (๐ โ ๐ด)โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฅ โ ๐ด โ๐ฃ โ (๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด))) |
27 | 22, 13, 26 | mp2an 691 |
. . . 4
โข
(โ๐ข โ
(๐ โ ๐ด)โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฅ โ ๐ด โ๐ฃ โ (๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด)) |
28 | 8 | sheli 29955 |
. . . . . . . 8
โข (๐ฅ โ ๐ด โ ๐ฅ โ โ) |
29 | 8 | sheli 29955 |
. . . . . . . 8
โข (๐ฆ โ ๐ด โ ๐ฆ โ โ) |
30 | 2 | lnopaddi 30712 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ฅ +โ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
31 | 28, 29, 30 | syl2an 597 |
. . . . . . 7
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ (๐โ(๐ฅ +โ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
32 | | shaddcl 29958 |
. . . . . . . . 9
โข ((๐ด โ
Sโ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ (๐ฅ +โ ๐ฆ) โ ๐ด) |
33 | 8, 32 | mp3an1 1449 |
. . . . . . . 8
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ (๐ฅ +โ ๐ฆ) โ ๐ด) |
34 | | funfvima2 7176 |
. . . . . . . . 9
โข ((Fun
๐ โง ๐ด โ dom ๐) โ ((๐ฅ +โ ๐ฆ) โ ๐ด โ (๐โ(๐ฅ +โ ๐ฆ)) โ (๐ โ ๐ด))) |
35 | 12, 15, 34 | mp2an 691 |
. . . . . . . 8
โข ((๐ฅ +โ ๐ฆ) โ ๐ด โ (๐โ(๐ฅ +โ ๐ฆ)) โ (๐ โ ๐ด)) |
36 | 33, 35 | syl 17 |
. . . . . . 7
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ (๐โ(๐ฅ +โ ๐ฆ)) โ (๐ โ ๐ด)) |
37 | 31, 36 | eqeltrrd 2840 |
. . . . . 6
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ด) โ ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
38 | 37 | ralrimiva 3142 |
. . . . 5
โข (๐ฅ โ ๐ด โ โ๐ฆ โ ๐ด ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
39 | | oveq2 7358 |
. . . . . . . 8
โข (๐ฃ = (๐โ๐ฆ) โ ((๐โ๐ฅ) +โ ๐ฃ) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
40 | 39 | eleq1d 2823 |
. . . . . . 7
โข (๐ฃ = (๐โ๐ฆ) โ (((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด) โ ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐ โ ๐ด))) |
41 | 40 | ralima 7183 |
. . . . . 6
โข ((๐ Fn โ โง ๐ด โ โ) โ
(โ๐ฃ โ (๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฆ โ ๐ด ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐ โ ๐ด))) |
42 | 22, 13, 41 | mp2an 691 |
. . . . 5
โข
(โ๐ฃ โ
(๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฆ โ ๐ด ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
43 | 38, 42 | sylibr 233 |
. . . 4
โข (๐ฅ โ ๐ด โ โ๐ฃ โ (๐ โ ๐ด)((๐โ๐ฅ) +โ ๐ฃ) โ (๐ โ ๐ด)) |
44 | 27, 43 | mprgbir 3070 |
. . 3
โข
โ๐ข โ
(๐ โ ๐ด)โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) |
45 | 2 | lnopmuli 30713 |
. . . . . . . 8
โข ((๐ข โ โ โง ๐ฆ โ โ) โ (๐โ(๐ข ยทโ ๐ฆ)) = (๐ข ยทโ (๐โ๐ฆ))) |
46 | 29, 45 | sylan2 594 |
. . . . . . 7
โข ((๐ข โ โ โง ๐ฆ โ ๐ด) โ (๐โ(๐ข ยทโ ๐ฆ)) = (๐ข ยทโ (๐โ๐ฆ))) |
47 | | shmulcl 29959 |
. . . . . . . . 9
โข ((๐ด โ
Sโ โง ๐ข โ โ โง ๐ฆ โ ๐ด) โ (๐ข ยทโ ๐ฆ) โ ๐ด) |
48 | 8, 47 | mp3an1 1449 |
. . . . . . . 8
โข ((๐ข โ โ โง ๐ฆ โ ๐ด) โ (๐ข ยทโ ๐ฆ) โ ๐ด) |
49 | | funfvima2 7176 |
. . . . . . . . 9
โข ((Fun
๐ โง ๐ด โ dom ๐) โ ((๐ข ยทโ ๐ฆ) โ ๐ด โ (๐โ(๐ข ยทโ ๐ฆ)) โ (๐ โ ๐ด))) |
50 | 12, 15, 49 | mp2an 691 |
. . . . . . . 8
โข ((๐ข
ยทโ ๐ฆ) โ ๐ด โ (๐โ(๐ข ยทโ ๐ฆ)) โ (๐ โ ๐ด)) |
51 | 48, 50 | syl 17 |
. . . . . . 7
โข ((๐ข โ โ โง ๐ฆ โ ๐ด) โ (๐โ(๐ข ยทโ ๐ฆ)) โ (๐ โ ๐ด)) |
52 | 46, 51 | eqeltrrd 2840 |
. . . . . 6
โข ((๐ข โ โ โง ๐ฆ โ ๐ด) โ (๐ข ยทโ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
53 | 52 | ralrimiva 3142 |
. . . . 5
โข (๐ข โ โ โ
โ๐ฆ โ ๐ด (๐ข ยทโ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
54 | | oveq2 7358 |
. . . . . . . 8
โข (๐ฃ = (๐โ๐ฆ) โ (๐ข ยทโ ๐ฃ) = (๐ข ยทโ (๐โ๐ฆ))) |
55 | 54 | eleq1d 2823 |
. . . . . . 7
โข (๐ฃ = (๐โ๐ฆ) โ ((๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด) โ (๐ข ยทโ (๐โ๐ฆ)) โ (๐ โ ๐ด))) |
56 | 55 | ralima 7183 |
. . . . . 6
โข ((๐ Fn โ โง ๐ด โ โ) โ
(โ๐ฃ โ (๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฆ โ ๐ด (๐ข ยทโ (๐โ๐ฆ)) โ (๐ โ ๐ด))) |
57 | 22, 13, 56 | mp2an 691 |
. . . . 5
โข
(โ๐ฃ โ
(๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด) โ โ๐ฆ โ ๐ด (๐ข ยทโ (๐โ๐ฆ)) โ (๐ โ ๐ด)) |
58 | 53, 57 | sylibr 233 |
. . . 4
โข (๐ข โ โ โ
โ๐ฃ โ (๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด)) |
59 | 58 | rgen 3065 |
. . 3
โข
โ๐ข โ
โ โ๐ฃ โ
(๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด) |
60 | 44, 59 | pm3.2i 472 |
. 2
โข
(โ๐ข โ
(๐ โ ๐ด)โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โง โ๐ข โ โ โ๐ฃ โ (๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด)) |
61 | | issh2 29950 |
. 2
โข ((๐ โ ๐ด) โ Sโ
โ (((๐ โ ๐ด) โ โ โง
0โ โ (๐ โ ๐ด)) โง (โ๐ข โ (๐ โ ๐ด)โ๐ฃ โ (๐ โ ๐ด)(๐ข +โ ๐ฃ) โ (๐ โ ๐ด) โง โ๐ข โ โ โ๐ฃ โ (๐ โ ๐ด)(๐ข ยทโ ๐ฃ) โ (๐ โ ๐ด)))) |
62 | 20, 60, 61 | mpbir2an 710 |
1
โข (๐ โ ๐ด) โ
Sโ |