Proof of Theorem mulgdir
Step | Hyp | Ref
| Expression |
1 | | mulgnndir.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
2 | | mulgnndir.t |
. . . 4
⊢ · =
(.g‘𝐺) |
3 | | mulgnndir.p |
. . . 4
⊢ + =
(+g‘𝐺) |
4 | 1, 2, 3 | mulgdirlem 17572 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
5 | 4 | 3expa 1265 |
. 2
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
6 | | simpll 790 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝐺 ∈ Grp) |
7 | | simpr2 1068 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℤ) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈
ℤ) |
9 | 8 | znegcld 11484 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -𝑁 ∈
ℤ) |
10 | | simpr1 1067 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈
ℤ) |
12 | 11 | znegcld 11484 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -𝑀 ∈
ℤ) |
13 | | simplr3 1105 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝑋 ∈ 𝐵) |
14 | 11 | zcnd 11483 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈
ℂ) |
15 | 8 | zcnd 11483 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈
ℂ) |
16 | 14, 15 | negdid 10405 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -(𝑀 + 𝑁) = (-𝑀 + -𝑁)) |
17 | 14 | negcld 10379 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -𝑀 ∈
ℂ) |
18 | 15 | negcld 10379 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -𝑁 ∈
ℂ) |
19 | 17, 18 | addcomd 10238 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (-𝑀 + -𝑁) = (-𝑁 + -𝑀)) |
20 | 16, 19 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -(𝑀 + 𝑁) = (-𝑁 + -𝑀)) |
21 | | simpr 477 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → -(𝑀 + 𝑁) ∈
ℕ0) |
22 | 20, 21 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (-𝑁 + -𝑀) ∈
ℕ0) |
23 | 1, 2, 3 | mulgdirlem 17572 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (-𝑁 ∈ ℤ ∧ -𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (-𝑁 + -𝑀) ∈ ℕ0) →
((-𝑁 + -𝑀) · 𝑋) = ((-𝑁 · 𝑋) + (-𝑀 · 𝑋))) |
24 | 6, 9, 12, 13, 22, 23 | syl131anc 1339 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((-𝑁 + -𝑀) · 𝑋) = ((-𝑁 · 𝑋) + (-𝑀 · 𝑋))) |
25 | 20 | oveq1d 6665 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
(-(𝑀 + 𝑁) · 𝑋) = ((-𝑁 + -𝑀) · 𝑋)) |
26 | 10, 7 | zaddcld 11486 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈ ℤ) |
27 | 26 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℤ) |
28 | | eqid 2622 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
29 | 1, 2, 28 | mulgneg 17560 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑀 + 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) |
30 | 6, 27, 13, 29 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
(-(𝑀 + 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) |
31 | 25, 30 | eqtr3d 2658 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((-𝑁 + -𝑀) · 𝑋) = ((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) |
32 | 1, 2, 28 | mulgneg 17560 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
33 | 6, 8, 13, 32 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
34 | 1, 2, 28 | mulgneg 17560 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑀 · 𝑋) = ((invg‘𝐺)‘(𝑀 · 𝑋))) |
35 | 6, 11, 13, 34 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (-𝑀 · 𝑋) = ((invg‘𝐺)‘(𝑀 · 𝑋))) |
36 | 33, 35 | oveq12d 6668 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((-𝑁 · 𝑋) + (-𝑀 · 𝑋)) = (((invg‘𝐺)‘(𝑁 · 𝑋)) +
((invg‘𝐺)‘(𝑀 · 𝑋)))) |
37 | 1, 2 | mulgcl 17559 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) ∈ 𝐵) |
38 | 6, 11, 13, 37 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (𝑀 · 𝑋) ∈ 𝐵) |
39 | 1, 2 | mulgcl 17559 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
40 | 6, 8, 13, 39 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → (𝑁 · 𝑋) ∈ 𝐵) |
41 | 1, 3, 28 | grpinvadd 17493 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑋) ∈ 𝐵 ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋))) = (((invg‘𝐺)‘(𝑁 · 𝑋)) +
((invg‘𝐺)‘(𝑀 · 𝑋)))) |
42 | 6, 38, 40, 41 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋))) = (((invg‘𝐺)‘(𝑁 · 𝑋)) +
((invg‘𝐺)‘(𝑀 · 𝑋)))) |
43 | 36, 42 | eqtr4d 2659 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((-𝑁 · 𝑋) + (-𝑀 · 𝑋)) = ((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋)))) |
44 | 24, 31, 43 | 3eqtr3d 2664 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋)) = ((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋)))) |
45 | 44 | fveq2d 6195 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) = ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋))))) |
46 | 1, 2 | mulgcl 17559 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) |
47 | 6, 27, 13, 46 | syl3anc 1326 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) |
48 | 1, 28 | grpinvinv 17482 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) = ((𝑀 + 𝑁) · 𝑋)) |
49 | 6, 47, 48 | syl2anc 693 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 + 𝑁) · 𝑋))) = ((𝑀 + 𝑁) · 𝑋)) |
50 | 1, 3 | grpcl 17430 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑋) ∈ 𝐵 ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) ∈ 𝐵) |
51 | 6, 38, 40, 50 | syl3anc 1326 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) ∈ 𝐵) |
52 | 1, 28 | grpinvinv 17482 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 · 𝑋) + (𝑁 · 𝑋)) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋)))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
53 | 6, 51, 52 | syl2anc 693 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) →
((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑋) + (𝑁 · 𝑋)))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
54 | 45, 49, 53 | 3eqtr3d 2664 |
. 2
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ -(𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
55 | | elznn0 11392 |
. . . 4
⊢ ((𝑀 + 𝑁) ∈ ℤ ↔ ((𝑀 + 𝑁) ∈ ℝ ∧ ((𝑀 + 𝑁) ∈ ℕ0 ∨ -(𝑀 + 𝑁) ∈
ℕ0))) |
56 | 55 | simprbi 480 |
. . 3
⊢ ((𝑀 + 𝑁) ∈ ℤ → ((𝑀 + 𝑁) ∈ ℕ0 ∨ -(𝑀 + 𝑁) ∈
ℕ0)) |
57 | 26, 56 | syl 17 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) ∈ ℕ0 ∨ -(𝑀 + 𝑁) ∈
ℕ0)) |
58 | 5, 54, 57 | mpjaodan 827 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |