Metamath Proof Explorer

Theorem oppgid

Description: Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
oppgid.2 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion oppgid 0 = ( 0g ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ 𝑂 = ( oppg ‘ 𝑅 )
2 oppgid.2 ⊢ 0 = ( 0g ‘ 𝑅 )
3 ancom ⊢ ( ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ) )
4 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
6 4 1 5 oppgplus ⊢ ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 )
7 6 eqeq1i ⊢ ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ↔ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 )
8 4 1 5 oppgplus ⊢ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 )
9 8 eqeq1i ⊢ ( ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ↔ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 )
10 7 9 anbi12i ⊢ ( ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ) )
11 3 10 bitr4i ⊢ ( ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) )
12 11 ralbii ⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) )
13 12 anbi2i ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) )
14 13 iotabii ⊢ ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 15 4 2 grpidval ⊢ 0 = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑦 ) ) )
17 1 15 oppgbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
18 eqid ⊢ ( 0g ‘ 𝑂 ) = ( 0g ‘ 𝑂 )
19 17 5 18 grpidval ⊢ ( 0g ‘ 𝑂 ) = ( ℩ 𝑥 ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑂 ) 𝑥 ) = 𝑦 ) ) )
20 14 16 19 3eqtr4i ⊢ 0 = ( 0g ‘ 𝑂 )