Metamath Proof Explorer

Theorem opprsubg

Description: Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprsubg ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
4 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5 1 4 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
6 3 5 grpprop ⊢ ( 𝑅 ∈ Grp ↔ 𝑂 ∈ Grp )
7 biid ⊢ ( 𝑥 ⊆ ( Base ‘ 𝑅 ) ↔ 𝑥 ⊆ ( Base ‘ 𝑅 ) )
8 eqid ⊢ ( 𝑅 ↾s 𝑥 ) = ( 𝑅 ↾s 𝑥 )
9 8 2 ressbas ⊢ ( 𝑥 ∈ V → ( 𝑥 ∩ ( Base ‘ 𝑅 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑥 ) ) )
10 9 elv ⊢ ( 𝑥 ∩ ( Base ‘ 𝑅 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑥 ) )
11 eqid ⊢ ( 𝑂 ↾s 𝑥 ) = ( 𝑂 ↾s 𝑥 )
12 11 3 ressbas ⊢ ( 𝑥 ∈ V → ( 𝑥 ∩ ( Base ‘ 𝑅 ) ) = ( Base ‘ ( 𝑂 ↾s 𝑥 ) ) )
13 12 elv ⊢ ( 𝑥 ∩ ( Base ‘ 𝑅 ) ) = ( Base ‘ ( 𝑂 ↾s 𝑥 ) )
14 10 13 eqtr3i ⊢ ( Base ‘ ( 𝑅 ↾s 𝑥 ) ) = ( Base ‘ ( 𝑂 ↾s 𝑥 ) )
15 8 4 ressplusg ⊢ ( 𝑥 ∈ V → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝑥 ) ) )
16 11 5 ressplusg ⊢ ( 𝑥 ∈ V → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑂 ↾s 𝑥 ) ) )
17 15 16 eqtr3d ⊢ ( 𝑥 ∈ V → ( +g ‘ ( 𝑅 ↾s 𝑥 ) ) = ( +g ‘ ( 𝑂 ↾s 𝑥 ) ) )
18 17 elv ⊢ ( +g ‘ ( 𝑅 ↾s 𝑥 ) ) = ( +g ‘ ( 𝑂 ↾s 𝑥 ) )
19 14 18 grpprop ⊢ ( ( 𝑅 ↾s 𝑥 ) ∈ Grp ↔ ( 𝑂 ↾s 𝑥 ) ∈ Grp )
20 6 7 19 3anbi123i ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ⊆ ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑥 ) ∈ Grp ) ↔ ( 𝑂 ∈ Grp ∧ 𝑥 ⊆ ( Base ‘ 𝑅 ) ∧ ( 𝑂 ↾s 𝑥 ) ∈ Grp ) )
21 2 issubg ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝑅 ∈ Grp ∧ 𝑥 ⊆ ( Base ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑥 ) ∈ Grp ) )
22 3 issubg ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝑂 ) ↔ ( 𝑂 ∈ Grp ∧ 𝑥 ⊆ ( Base ‘ 𝑅 ) ∧ ( 𝑂 ↾s 𝑥 ) ∈ Grp ) )
23 20 21 22 3bitr4i ⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝑂 ) )
24 23 eqriv ⊢ ( SubGrp ‘ 𝑅 ) = ( SubGrp ‘ 𝑂 )