Metamath Proof Explorer

Theorem oppgsubm

Description: Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis oppggic.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
Assertion oppgsubm ( SubMnd ‘ 𝐺 ) = ( SubMnd ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppggic.o ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 submrcl ⊢ ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
3 submrcl ⊢ ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) → 𝑂 ∈ Mnd )
4 1 oppgmndb ⊢ ( 𝐺 ∈ Mnd ↔ 𝑂 ∈ Mnd )
5 3 4 sylibr ⊢ ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) → 𝐺 ∈ Mnd )
6 ralcom ⊢ ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 eqid ⊢ ( +g ‘ 𝑂 ) = ( +g ‘ 𝑂 )
9 7 1 8 oppgplus ⊢ ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 )
10 9 eleq1i ⊢ ( ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 )
11 10 2ralbii ⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 )
12 6 11 bitr4i ⊢ ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 )
13 12 3anbi3i ⊢ ( ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) )
14 13 a1i ⊢ ( 𝐺 ∈ Mnd → ( ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
15 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
16 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
17 15 16 7 issubm ⊢ ( 𝐺 ∈ Mnd → ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ) ) )
18 1 15 oppgbas ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑂 )
19 1 16 oppgid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑂 )
20 18 19 8 issubm ⊢ ( 𝑂 ∈ Mnd → ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
21 4 20 sylbi ⊢ ( 𝐺 ∈ Mnd → ( 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑦 ∈ 𝑥 ( 𝑧 ( +g ‘ 𝑂 ) 𝑦 ) ∈ 𝑥 ) ) )
22 14 17 21 3bitr4d ⊢ ( 𝐺 ∈ Mnd → ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubMnd ‘ 𝑂 ) ) )
23 2 5 22 pm5.21nii ⊢ ( 𝑥 ∈ ( SubMnd ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubMnd ‘ 𝑂 ) )
24 23 eqriv ⊢ ( SubMnd ‘ 𝐺 ) = ( SubMnd ‘ 𝑂 )