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 \in Grp \leftrightarrow O \in Grp$
7		biid	$⊢ x \subseteq {Base}_{R} \leftrightarrow x \subseteq {Base}_{R}$
8		eqid	$⊢ R ↾_{𝑠} x = R ↾_{𝑠} x$
9	8 2	ressbas	$⊢ x \in V \to x \cap {Base}_{R} = {Base}_{(R ↾_{𝑠} x)}$
10	9	elv	$⊢ x \cap {Base}_{R} = {Base}_{(R ↾_{𝑠} x)}$
11		eqid	$⊢ O ↾_{𝑠} x = O ↾_{𝑠} x$
12	11 3	ressbas	$⊢ x \in V \to x \cap {Base}_{R} = {Base}_{(O ↾_{𝑠} x)}$
13	12	elv	$⊢ x \cap {Base}_{R} = {Base}_{(O ↾_{𝑠} x)}$
14	10 13	eqtr3i	$⊢ {Base}_{(R ↾_{𝑠} x)} = {Base}_{(O ↾_{𝑠} x)}$
15	8 4	ressplusg	$⊢ x \in V \to +_{R} = +_{(R ↾_{𝑠} x)}$
16	11 5	ressplusg	$⊢ x \in V \to +_{R} = +_{(O ↾_{𝑠} x)}$
17	15 16	eqtr3d	$⊢ x \in V \to +_{(R ↾_{𝑠} x)} = +_{(O ↾_{𝑠} x)}$
18	17	elv	$⊢ +_{(R ↾_{𝑠} x)} = +_{(O ↾_{𝑠} x)}$
19	14 18	grpprop	$⊢ R ↾_{𝑠} x \in Grp \leftrightarrow O ↾_{𝑠} x \in Grp$
20	6 7 19	3anbi123i	$⊢ (R \in Grp \land x \subseteq {Base}_{R} \land R ↾_{𝑠} x \in Grp) \leftrightarrow (O \in Grp \land x \subseteq {Base}_{R} \land O ↾_{𝑠} x \in Grp)$
21	2	issubg	$⊢ x \in SubGrp (R) \leftrightarrow (R \in Grp \land x \subseteq {Base}_{R} \land R ↾_{𝑠} x \in Grp)$
22	3	issubg	$⊢ x \in SubGrp (O) \leftrightarrow (O \in Grp \land x \subseteq {Base}_{R} \land O ↾_{𝑠} x \in Grp)$
23	20 21 22	3bitr4i	$⊢ x \in SubGrp (R) \leftrightarrow x \in SubGrp (O)$
24	23	eqriv	$⊢ SubGrp (R) = SubGrp (O)$

Metamath Proof Explorer

Theorem opprsubg

Proof