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 ⊢ O = opp r ⁡ R
Assertion opprsubg ⊢ SubGrp ⁡ R = SubGrp ⁡ O

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ O = opp r ⁡ R
2 eqid ⊢ Base R = Base R
3 1 2 opprbas ⊢ Base R = Base O
4 eqid ⊢ + R = + R
5 1 4 oppradd ⊢ + R = + O
6 3 5 grpprop ⊢ R ∈ Grp ↔ O ∈ Grp
7 biid ⊢ x ⊆ Base R ↔ x ⊆ Base R
8 eqid ⊢ R ↾ 𝑠 x = R ↾ 𝑠 x
9 8 2 ressbas ⊢ x ∈ V → x ∩ Base R = Base R ↾ 𝑠 x
10 9 elv ⊢ x ∩ Base R = Base R ↾ 𝑠 x
11 eqid ⊢ O ↾ 𝑠 x = O ↾ 𝑠 x
12 11 3 ressbas ⊢ x ∈ V → x ∩ Base R = Base O ↾ 𝑠 x
13 12 elv ⊢ x ∩ Base R = Base O ↾ 𝑠 x
14 10 13 eqtr3i ⊢ Base R ↾ 𝑠 x = Base O ↾ 𝑠 x
15 8 4 ressplusg ⊢ x ∈ V → + R = + R ↾ 𝑠 x
16 11 5 ressplusg ⊢ x ∈ V → + R = + O ↾ 𝑠 x
17 15 16 eqtr3d ⊢ x ∈ V → + R ↾ 𝑠 x = + O ↾ 𝑠 x
18 17 elv ⊢ + R ↾ 𝑠 x = + O ↾ 𝑠 x
19 14 18 grpprop ⊢ R ↾ 𝑠 x ∈ Grp ↔ O ↾ 𝑠 x ∈ Grp
20 6 7 19 3anbi123i ⊢ R ∈ Grp ∧ x ⊆ Base R ∧ R ↾ 𝑠 x ∈ Grp ↔ O ∈ Grp ∧ x ⊆ Base R ∧ O ↾ 𝑠 x ∈ Grp
21 2 issubg ⊢ x ∈ SubGrp ⁡ R ↔ R ∈ Grp ∧ x ⊆ Base R ∧ R ↾ 𝑠 x ∈ Grp
22 3 issubg ⊢ x ∈ SubGrp ⁡ O ↔ O ∈ Grp ∧ x ⊆ Base R ∧ O ↾ 𝑠 x ∈ Grp
23 20 21 22 3bitr4i ⊢ x ∈ SubGrp ⁡ R ↔ x ∈ SubGrp ⁡ O
24 23 eqriv ⊢ SubGrp ⁡ R = SubGrp ⁡ O