This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )