Step |
Hyp |
Ref |
Expression |
1 |
|
odcl.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
odcl.2 |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
odid.3 |
⊢ · = ( .g ‘ 𝐺 ) |
4 |
|
odid.4 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
5 |
|
oveq1 |
⊢ ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0 · 𝐴 ) ) |
6 |
1 4 3
|
mulg0 |
⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = 0 ) |
7 |
5 6
|
sylan9eqr |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) |
8 |
7
|
adantrr |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑂 ‘ 𝐴 ) = 0 ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ ) ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) |
9 |
|
oveq1 |
⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( 𝑦 · 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ) |
10 |
9
|
eqeq1d |
⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) ) |
11 |
10
|
elrab |
⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) ) |
12 |
11
|
simprbi |
⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) |
13 |
12
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) |
14 |
|
eqid |
⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } |
15 |
1 3 4 2 14
|
odlem1 |
⊢ ( 𝐴 ∈ 𝑋 → ( ( ( 𝑂 ‘ 𝐴 ) = 0 ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ ) ∨ ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) ) |
16 |
8 13 15
|
mpjaodan |
⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) |