Step | Hyp | Ref
| Expression |
1 | | oveq1 7416 |
. . . 4
โข (๐ = 0 โ (๐(.gโโ*๐ )๐ต) =
(0(.gโโ*๐ )๐ต)) |
2 | | oveq1 7416 |
. . . 4
โข (๐ = 0 โ (๐ ยทe ๐ต) = (0 ยทe ๐ต)) |
3 | 1, 2 | eqeq12d 2749 |
. . 3
โข (๐ = 0 โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ
(0(.gโโ*๐ )๐ต) = (0 ยทe ๐ต))) |
4 | | oveq1 7416 |
. . . 4
โข (๐ = ๐ โ (๐(.gโโ*๐ )๐ต) = (๐(.gโโ*๐ )๐ต)) |
5 | | oveq1 7416 |
. . . 4
โข (๐ = ๐ โ (๐ ยทe ๐ต) = (๐ ยทe ๐ต)) |
6 | 4, 5 | eqeq12d 2749 |
. . 3
โข (๐ = ๐ โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต))) |
7 | | oveq1 7416 |
. . . 4
โข (๐ = (๐ + 1) โ (๐(.gโโ*๐ )๐ต) = ((๐ +
1)(.gโโ*๐ )๐ต)) |
8 | | oveq1 7416 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ ยทe ๐ต) = ((๐ + 1) ยทe ๐ต)) |
9 | 7, 8 | eqeq12d 2749 |
. . 3
โข (๐ = (๐ + 1) โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ ((๐
+ 1)(.gโโ*๐ )๐ต) = ((๐ + 1)
ยทe ๐ต))) |
10 | | oveq1 7416 |
. . . 4
โข (๐ = -๐ โ (๐(.gโโ*๐ )๐ต) = (-๐(.gโโ*๐ )๐ต)) |
11 | | oveq1 7416 |
. . . 4
โข (๐ = -๐ โ (๐ ยทe ๐ต) = (-๐ ยทe ๐ต)) |
12 | 10, 11 | eqeq12d 2749 |
. . 3
โข (๐ = -๐ โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ (-๐(.gโโ*๐ )๐ต) = (-๐ ยทe ๐ต))) |
13 | | oveq1 7416 |
. . . 4
โข (๐ = ๐ด โ (๐(.gโโ*๐ )๐ต) = (๐ด(.gโโ*๐ )๐ต)) |
14 | | oveq1 7416 |
. . . 4
โข (๐ = ๐ด โ (๐ ยทe ๐ต) = (๐ด ยทe ๐ต)) |
15 | 13, 14 | eqeq12d 2749 |
. . 3
โข (๐ = ๐ด โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ (๐ด(.gโโ*๐ )๐ต) = (๐ด ยทe ๐ต))) |
16 | | xrsbas 20961 |
. . . . 5
โข
โ* =
(Baseโโ*๐ ) |
17 | | xrs0 32176 |
. . . . 5
โข 0 =
(0gโโ*๐ ) |
18 | | eqid 2733 |
. . . . 5
โข
(.gโโ*๐ ) =
(.gโโ*๐ ) |
19 | 16, 17, 18 | mulg0 18957 |
. . . 4
โข (๐ต โ โ*
โ (0(.gโโ*๐ )๐ต) = 0) |
20 | | xmul02 13247 |
. . . 4
โข (๐ต โ โ*
โ (0 ยทe ๐ต) = 0) |
21 | 19, 20 | eqtr4d 2776 |
. . 3
โข (๐ต โ โ*
โ (0(.gโโ*๐ )๐ต) = (0 ยทe
๐ต)) |
22 | | simpr 486 |
. . . . . 6
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) |
23 | 22 | oveq1d 7424 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐(.gโโ*๐ )๐ต) +๐ ๐ต) = ((๐
ยทe ๐ต) +๐
๐ต)) |
24 | | simpr 486 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ โ โ) โ ๐ โ โ) |
25 | | simpll 766 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ โ โ) โ ๐ต โ
โ*) |
26 | | xrsadd 20962 |
. . . . . . . . 9
โข
+๐ =
(+gโโ*๐ ) |
27 | 16, 18, 26 | mulgnnp1 18962 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ต โ โ*)
โ ((๐ +
1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
28 | 24, 25, 27 | syl2anc 585 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ โ โ) โ ((๐ +
1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
29 | | simpr 486 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ = 0) โ ๐ = 0) |
30 | | simpll 766 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ = 0) โ ๐ต โ
โ*) |
31 | | xaddlid 13221 |
. . . . . . . . . 10
โข (๐ต โ โ*
โ (0 +๐ ๐ต) = ๐ต) |
32 | 31 | adantl 483 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ต โ โ*) โ (0
+๐ ๐ต) =
๐ต) |
33 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ = 0 โง ๐ต โ โ*) โ ๐ = 0) |
34 | 33 | oveq1d 7424 |
. . . . . . . . . . 11
โข ((๐ = 0 โง ๐ต โ โ*) โ (๐(.gโโ*๐ )๐ต) =
(0(.gโโ*๐ )๐ต)) |
35 | 19 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ = 0 โง ๐ต โ โ*) โ
(0(.gโโ*๐ )๐ต) = 0) |
36 | 34, 35 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ต โ โ*) โ (๐(.gโโ*๐ )๐ต) = 0) |
37 | 36 | oveq1d 7424 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ต โ โ*) โ ((๐(.gโโ*๐ )๐ต) +๐ ๐ต) = (0 +๐ ๐ต)) |
38 | 33 | oveq1d 7424 |
. . . . . . . . . . . 12
โข ((๐ = 0 โง ๐ต โ โ*) โ (๐ + 1) = (0 +
1)) |
39 | | 0p1e1 12334 |
. . . . . . . . . . . 12
โข (0 + 1) =
1 |
40 | 38, 39 | eqtrdi 2789 |
. . . . . . . . . . 11
โข ((๐ = 0 โง ๐ต โ โ*) โ (๐ + 1) = 1) |
41 | 40 | oveq1d 7424 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ต โ โ*) โ ((๐ +
1)(.gโโ*๐ )๐ต) =
(1(.gโโ*๐ )๐ต)) |
42 | 16, 18 | mulg1 18961 |
. . . . . . . . . . 11
โข (๐ต โ โ*
โ (1(.gโโ*๐ )๐ต) = ๐ต) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ต โ โ*) โ
(1(.gโโ*๐ )๐ต) = ๐ต) |
44 | 41, 43 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ต โ โ*) โ ((๐ +
1)(.gโโ*๐ )๐ต) = ๐ต) |
45 | 32, 37, 44 | 3eqtr4rd 2784 |
. . . . . . . 8
โข ((๐ = 0 โง ๐ต โ โ*) โ ((๐ +
1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
46 | 29, 30, 45 | syl2anc 585 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง ๐ = 0) โ ((๐ +
1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
47 | | simpr 486 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ โ
โ0) โ ๐ โ โ0) |
48 | | elnn0 12474 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
49 | 47, 48 | sylib 217 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ โ
โ0) โ (๐ โ โ โจ ๐ = 0)) |
50 | 28, 46, 49 | mpjaodan 958 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ โ
โ0) โ ((๐ +
1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
51 | 50 | adantr 482 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
+ 1)(.gโโ*๐ )๐ต) = ((๐(.gโโ*๐ )๐ต) +๐ ๐ต)) |
52 | | nn0ssre 12476 |
. . . . . . . . 9
โข
โ0 โ โ |
53 | | ressxr 11258 |
. . . . . . . . 9
โข โ
โ โ* |
54 | 52, 53 | sstri 3992 |
. . . . . . . 8
โข
โ0 โ โ* |
55 | 47 | adantr 482 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ๐
โ โ0) |
56 | 54, 55 | sselid 3981 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ๐
โ โ*) |
57 | | nn0ge0 12497 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โค ๐) |
58 | 57 | ad2antlr 726 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ 0 โค ๐) |
59 | | 1xr 11273 |
. . . . . . . 8
โข 1 โ
โ* |
60 | 59 | a1i 11 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ 1 โ โ*) |
61 | | 0le1 11737 |
. . . . . . . 8
โข 0 โค
1 |
62 | 61 | a1i 11 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ 0 โค 1) |
63 | | simpll 766 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ๐ต
โ โ*) |
64 | | xadddi2r 13277 |
. . . . . . 7
โข (((๐ โ โ*
โง 0 โค ๐) โง (1
โ โ* โง 0 โค 1) โง ๐ต โ โ*) โ ((๐ +๐ 1)
ยทe ๐ต) =
((๐ ยทe
๐ต) +๐ (1
ยทe ๐ต))) |
65 | 56, 58, 60, 62, 63, 64 | syl221anc 1382 |
. . . . . 6
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
+๐ 1) ยทe ๐ต)
= ((๐ ยทe ๐ต) +๐ (1 ยทe ๐ต))) |
66 | 52, 55 | sselid 3981 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ๐
โ โ) |
67 | | 1re 11214 |
. . . . . . . . 9
โข 1 โ
โ |
68 | 67 | a1i 11 |
. . . . . . . 8
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ 1 โ โ) |
69 | | rexadd 13211 |
. . . . . . . 8
โข ((๐ โ โ โง 1 โ
โ) โ (๐
+๐ 1) = (๐ + 1)) |
70 | 66, 68, 69 | syl2anc 585 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (๐
+๐ 1) = (๐ +
1)) |
71 | 70 | oveq1d 7424 |
. . . . . 6
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
+๐ 1) ยทe ๐ต)
= ((๐ + 1) ยทe ๐ต)) |
72 | | xmullid 13259 |
. . . . . . . 8
โข (๐ต โ โ*
โ (1 ยทe ๐ต) = ๐ต) |
73 | 63, 72 | syl 17 |
. . . . . . 7
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (1 ยทe ๐ต) = ๐ต) |
74 | 73 | oveq2d 7425 |
. . . . . 6
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
ยทe ๐ต) +๐ (1
ยทe ๐ต)) = ((๐ ยทe ๐ต) +๐ ๐ต)) |
75 | 65, 71, 74 | 3eqtr3d 2781 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
+ 1) ยทe ๐ต) = ((๐ ยทe ๐ต) +๐ ๐ต)) |
76 | 23, 51, 75 | 3eqtr4d 2783 |
. . . 4
โข (((๐ต โ โ*
โง ๐ โ
โ0) โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ ((๐
+ 1)(.gโโ*๐ )๐ต) = ((๐ + 1)
ยทe ๐ต)) |
77 | 76 | exp31 421 |
. . 3
โข (๐ต โ โ*
โ (๐ โ
โ0 โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ ((๐
+ 1)(.gโโ*๐ )๐ต) = ((๐ + 1)
ยทe ๐ต)))) |
78 | | xnegeq 13186 |
. . . . . 6
โข ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ -๐(๐(.gโโ*๐ )๐ต) = -๐(๐ ยทe ๐ต)) |
79 | 78 | adantl 483 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ โ)
โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ -๐(๐(.gโโ*๐ )๐ต) = -๐(๐ ยทe ๐ต)) |
80 | | eqid 2733 |
. . . . . . . . 9
โข
(invgโโ*๐ ) =
(invgโโ*๐ ) |
81 | 16, 18, 80 | mulgnegnn 18964 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ต โ โ*)
โ (-๐(.gโโ*๐ )๐ต) =
((invgโโ*๐ )โ(๐(.gโโ*๐ )๐ต))) |
82 | 81 | ancoms 460 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (-๐(.gโโ*๐ )๐ต) =
((invgโโ*๐ )โ(๐(.gโโ*๐ )๐ต))) |
83 | | xrsex 20960 |
. . . . . . . . . . . 12
โข
โ*๐ โ V |
84 | 83 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ
โ*๐ โ V) |
85 | | ssidd 4006 |
. . . . . . . . . . 11
โข (๐ โ โ โ
โ* โ โ*) |
86 | | simp2 1138 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฅ โ โ*
โง ๐ฆ โ
โ*) โ ๐ฅ โ โ*) |
87 | | simp3 1139 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฅ โ โ*
โง ๐ฆ โ
โ*) โ ๐ฆ โ โ*) |
88 | 86, 87 | xaddcld 13280 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฅ โ โ*
โง ๐ฆ โ
โ*) โ (๐ฅ +๐ ๐ฆ) โ
โ*) |
89 | 16, 18, 26, 84, 85, 88 | mulgnnsubcl 18966 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ โง ๐ต โ โ*)
โ (๐(.gโโ*๐ )๐ต) โ โ*) |
90 | 89 | 3anidm12 1420 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ต โ โ*)
โ (๐(.gโโ*๐ )๐ต) โ โ*) |
91 | 90 | ancoms 460 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (๐(.gโโ*๐ )๐ต) โ โ*) |
92 | | xrsinvgval 32178 |
. . . . . . . 8
โข ((๐(.gโโ*๐ )๐ต) โ โ* โ
((invgโโ*๐ )โ(๐(.gโโ*๐ )๐ต)) = -๐(๐(.gโโ*๐ )๐ต)) |
93 | 91, 92 | syl 17 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ โ โ)
โ
((invgโโ*๐ )โ(๐(.gโโ*๐ )๐ต)) = -๐(๐(.gโโ*๐ )๐ต)) |
94 | 82, 93 | eqtrd 2773 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (-๐(.gโโ*๐ )๐ต) = -๐(๐(.gโโ*๐ )๐ต)) |
95 | 94 | adantr 482 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ โ)
โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (-๐(.gโโ*๐ )๐ต) = -๐(๐(.gโโ*๐ )๐ต)) |
96 | | nnre 12219 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
97 | 96 | adantl 483 |
. . . . . . . . 9
โข ((๐ต โ โ*
โง ๐ โ โ)
โ ๐ โ
โ) |
98 | | rexneg 13190 |
. . . . . . . . 9
โข (๐ โ โ โ
-๐๐ =
-๐) |
99 | 97, 98 | syl 17 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ โ โ)
โ -๐๐ = -๐) |
100 | 99 | oveq1d 7424 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (-๐๐ ยทe ๐ต) = (-๐ ยทe ๐ต)) |
101 | | nnssre 12216 |
. . . . . . . . . 10
โข โ
โ โ |
102 | 101, 53 | sstri 3992 |
. . . . . . . . 9
โข โ
โ โ* |
103 | | simpr 486 |
. . . . . . . . 9
โข ((๐ต โ โ*
โง ๐ โ โ)
โ ๐ โ
โ) |
104 | 102, 103 | sselid 3981 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ โ โ)
โ ๐ โ
โ*) |
105 | | simpl 484 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ โ โ)
โ ๐ต โ
โ*) |
106 | | xmulneg1 13248 |
. . . . . . . 8
โข ((๐ โ โ*
โง ๐ต โ
โ*) โ (-๐๐ ยทe ๐ต) = -๐(๐ ยทe ๐ต)) |
107 | 104, 105,
106 | syl2anc 585 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (-๐๐ ยทe ๐ต) = -๐(๐ ยทe ๐ต)) |
108 | 100, 107 | eqtr3d 2775 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ โ โ)
โ (-๐
ยทe ๐ต) =
-๐(๐
ยทe ๐ต)) |
109 | 108 | adantr 482 |
. . . . 5
โข (((๐ต โ โ*
โง ๐ โ โ)
โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (-๐
ยทe ๐ต) =
-๐(๐ ยทe
๐ต)) |
110 | 79, 95, 109 | 3eqtr4d 2783 |
. . . 4
โข (((๐ต โ โ*
โง ๐ โ โ)
โง (๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต)) โ (-๐(.gโโ*๐ )๐ต) = (-๐ ยทe ๐ต)) |
111 | 110 | exp31 421 |
. . 3
โข (๐ต โ โ*
โ (๐ โ โ
โ ((๐(.gโโ*๐ )๐ต) = (๐ ยทe ๐ต) โ (-๐(.gโโ*๐ )๐ต) = (-๐ ยทe ๐ต)))) |
112 | 3, 6, 9, 12, 15, 21, 77, 111 | zindd 12663 |
. 2
โข (๐ต โ โ*
โ (๐ด โ โค
โ (๐ด(.gโโ*๐ )๐ต) = (๐ด ยทe ๐ต))) |
113 | 112 | impcom 409 |
1
โข ((๐ด โ โค โง ๐ต โ โ*)
โ (๐ด(.gโโ*๐ )๐ต) = (๐ด ยทe ๐ต)) |