Step | Hyp | Ref
| Expression |
1 | | 0sno 27710 |
. . 3
โข
0s โ No |
2 | | mulsval 27960 |
. . 3
โข ((๐ด โ
No โง 0s โ No ) โ
(๐ด ยทs
0s ) = (({๐
โฃ โ๐ โ ( L
โ๐ด)โ๐ โ ( L โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ ))})
|s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |
3 | 1, 2 | mpan2 688 |
. 2
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = (({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))}
โช {๐ โฃ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |
4 | | rex0 4352 |
. . . . . . . . . 10
โข ยฌ
โ๐ โ โ
๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐)) |
5 | | left0s 27770 |
. . . . . . . . . . 11
โข ( L
โ 0s ) = โ
|
6 | 5 | rexeqi 3318 |
. . . . . . . . . 10
โข
(โ๐ โ ( L
โ 0s )๐ =
(((๐ ยทs
0s ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ โ
๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))) |
7 | 4, 6 | mtbir 323 |
. . . . . . . . 9
โข ยฌ
โ๐ โ ( L โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) |
8 | 7 | a1i 11 |
. . . . . . . 8
โข (๐ โ ( L โ๐ด) โ ยฌ โ๐ โ ( L โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
9 | 8 | nrex 3068 |
. . . . . . 7
โข ยฌ
โ๐ โ ( L
โ๐ด)โ๐ โ ( L โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) |
10 | 9 | abf 4397 |
. . . . . 6
โข {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))} =
โ
|
11 | | rex0 4352 |
. . . . . . . . . 10
โข ยฌ
โ๐ โ โ
๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ )) |
12 | | right0s 27771 |
. . . . . . . . . . 11
โข ( R
โ 0s ) = โ
|
13 | 12 | rexeqi 3318 |
. . . . . . . . . 10
โข
(โ๐ โ ( R
โ 0s )๐ =
(((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ๐ โ โ
๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ ))) |
14 | 11, 13 | mtbir 323 |
. . . . . . . . 9
โข ยฌ
โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) |
15 | 14 | a1i 11 |
. . . . . . . 8
โข (๐ โ ( R โ๐ด) โ ยฌ โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
16 | 15 | nrex 3068 |
. . . . . . 7
โข ยฌ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) |
17 | 16 | abf 4397 |
. . . . . 6
โข {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ ))} =
โ
|
18 | 10, 17 | uneq12i 4156 |
. . . . 5
โข ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))}
โช {๐ โฃ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) = (โ
โช
โ
) |
19 | | un0 4385 |
. . . . 5
โข (โ
โช โ
) = โ
|
20 | 18, 19 | eqtri 2754 |
. . . 4
โข ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))}
โช {๐ โฃ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) = โ
|
21 | | rex0 4352 |
. . . . . . . . . 10
โข ยฌ
โ๐ข โ โ
๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข)) |
22 | 12 | rexeqi 3318 |
. . . . . . . . . 10
โข
(โ๐ข โ ( R
โ 0s )๐ =
(((๐ก ยทs
0s ) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ โ๐ข โ โ
๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))) |
23 | 21, 22 | mtbir 323 |
. . . . . . . . 9
โข ยฌ
โ๐ข โ ( R โ
0s )๐ = (((๐ก ยทs
0s ) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) |
24 | 23 | a1i 11 |
. . . . . . . 8
โข (๐ก โ ( L โ๐ด) โ ยฌ โ๐ข โ ( R โ
0s )๐ = (((๐ก ยทs
0s ) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) |
25 | 24 | nrex 3068 |
. . . . . . 7
โข ยฌ
โ๐ก โ ( L
โ๐ด)โ๐ข โ ( R โ
0s )๐ = (((๐ก ยทs
0s ) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) |
26 | 25 | abf 4397 |
. . . . . 6
โข {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))} =
โ
|
27 | | rex0 4352 |
. . . . . . . . . 10
โข ยฌ
โ๐ค โ โ
๐ = (((๐ฃ ยทs 0s )
+s (๐ด
ยทs ๐ค))
-s (๐ฃ
ยทs ๐ค)) |
28 | 5 | rexeqi 3318 |
. . . . . . . . . 10
โข
(โ๐ค โ ( L
โ 0s )๐ =
(((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ โ๐ค โ โ
๐ = (((๐ฃ ยทs 0s )
+s (๐ด
ยทs ๐ค))
-s (๐ฃ
ยทs ๐ค))) |
29 | 27, 28 | mtbir 323 |
. . . . . . . . 9
โข ยฌ
โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) |
30 | 29 | a1i 11 |
. . . . . . . 8
โข (๐ฃ โ ( R โ๐ด) โ ยฌ โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) |
31 | 30 | nrex 3068 |
. . . . . . 7
โข ยฌ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) |
32 | 31 | abf 4397 |
. . . . . 6
โข {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ 0s )๐ = (((๐ฃ ยทs 0s )
+s (๐ด
ยทs ๐ค))
-s (๐ฃ
ยทs ๐ค))} =
โ
|
33 | 26, 32 | uneq12i 4156 |
. . . . 5
โข ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) = (โ
โช
โ
) |
34 | 33, 19 | eqtri 2754 |
. . . 4
โข ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) = โ
|
35 | 20, 34 | oveq12i 7416 |
. . 3
โข (({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))}
โช {๐ โฃ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) = (โ
|s โ
) |
36 | | df-0s 27708 |
. . 3
โข
0s = (โ
|s โ
) |
37 | 35, 36 | eqtr4i 2757 |
. 2
โข (({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ 0s )๐ = (((๐ ยทs 0s )
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))}
โช {๐ โฃ
โ๐ โ ( R
โ๐ด)โ๐ โ ( R โ
0s )๐ = (((๐ ยทs
0s ) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ 0s )๐ = (((๐ก ยทs 0s )
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))}
โช {๐ โฃ
โ๐ฃ โ ( R
โ๐ด)โ๐ค โ ( L โ
0s )๐ = (((๐ฃ ยทs
0s ) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) = 0s |
38 | 3, 37 | eqtrdi 2782 |
1
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |