Metamath Proof Explorer

Theorem oppgmnd

Description: The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypothesis oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
Assertion oppgmnd ( 𝑅 ∈ Mnd → 𝑂 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 oppgbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝑅 ∈ Mnd → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
5 eqidd ⊢ ( 𝑅 ∈ Mnd → ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 ) )
6 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
8 6 1 7 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 )
9 2 6 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
10 9 3com23 ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
11 8 10 eqeltrid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
12 simpl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Mnd )
13 simpr3 ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
14 simpr2 ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
15 simpr1 ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
16 2 6 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ) )
17 12 13 14 15 16 syl13anc ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ) )
18 17 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑧 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑥 ) )
19 8 oveq1i ⊢ ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑂 ) 𝑧 ) = ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑂 ) 𝑧 )
20 6 1 7 oppgplus ⊢ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) )
21 19 20 eqtri ⊢ ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) )
22 6 1 7 oppgplus ⊢ ( 𝑦 ( +g ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 )
23 22 oveq2i ⊢ ( 𝑥 ( +g ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑂 ) 𝑧 ) ) = ( 𝑥 ( +g ‘ 𝑂 ) ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) )
24 6 1 7 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑥 )
25 23 24 eqtri ⊢ ( 𝑥 ( +g ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑂 ) 𝑧 ) ) = ( ( 𝑧 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑥 )
26 18 21 25 3eqtr4g ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑂 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑂 ) 𝑧 ) ) )
27 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
28 2 27 mndidcl ⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29 6 1 7 oppgplus ⊢ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) )
30 2 6 27 mndrid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = 𝑥 )
31 29 30 syl5eq ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑂 ) 𝑥 ) = 𝑥 )
32 6 1 7 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑥 )
33 2 6 27 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
34 32 33 syl5eq ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑂 ) ( 0g ‘ 𝑅 ) ) = 𝑥 )
35 4 5 11 26 28 31 34 ismndd ⊢ ( 𝑅 ∈ Mnd → 𝑂 ∈ Mnd )