Step |
Hyp |
Ref |
Expression |
1 |
|
oppgbas.1 |
⊢ 𝑂 = ( oppg ‘ 𝑅 ) |
2 |
1
|
oppgmnd |
⊢ ( 𝑅 ∈ Mnd → 𝑂 ∈ Mnd ) |
3 |
|
eqid |
⊢ ( oppg ‘ 𝑂 ) = ( oppg ‘ 𝑂 ) |
4 |
3
|
oppgmnd |
⊢ ( 𝑂 ∈ Mnd → ( oppg ‘ 𝑂 ) ∈ Mnd ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
6 |
1 5
|
oppgbas |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) |
7 |
3 6
|
oppgbas |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppg ‘ 𝑂 ) ) |
8 |
7
|
a1i |
⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( oppg ‘ 𝑂 ) ) ) |
9 |
|
eqidd |
⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) |
10 |
|
eqid |
⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 ) |
11 |
|
eqid |
⊢ ( +g ‘ ( oppg ‘ 𝑂 ) ) = ( +g ‘ ( oppg ‘ 𝑂 ) ) |
12 |
10 3 11
|
oppgplus |
⊢ ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) |
13 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
14 |
13 1 10
|
oppgplus |
⊢ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) |
15 |
12 14
|
eqtri |
⊢ ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) |
16 |
15
|
a1i |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ ( oppg ‘ 𝑂 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) |
17 |
8 9 16
|
mndpropd |
⊢ ( ⊤ → ( ( oppg ‘ 𝑂 ) ∈ Mnd ↔ 𝑅 ∈ Mnd ) ) |
18 |
17
|
mptru |
⊢ ( ( oppg ‘ 𝑂 ) ∈ Mnd ↔ 𝑅 ∈ Mnd ) |
19 |
4 18
|
sylib |
⊢ ( 𝑂 ∈ Mnd → 𝑅 ∈ Mnd ) |
20 |
2 19
|
impbii |
⊢ ( 𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd ) |