Metamath Proof Explorer


Theorem oppgmndb

Description: Bidirectional form of oppgmnd . (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppgbas.1 𝑂 = ( oppg𝑅 )
Assertion oppgmndb ( 𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd )

Proof

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 )