oppr2idl

Description: Two sided ideal of the opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Step	Hyp	Ref	Expression
1		oppreqg.o	$⊢ O = {opp}_{r} (R)$
2		oppr2idl.2	$⊢ φ \to R \in Ring$
3		incom	$⊢ LIdeal (R) \cap LIdeal (O) = LIdeal (O) \cap LIdeal (R)$
4	1 2	opprlidlabs	$⊢ φ \to LIdeal (R) = LIdeal ({opp}_{r} (O))$
5	4	ineq2d	$⊢ φ \to LIdeal (O) \cap LIdeal (R) = LIdeal (O) \cap LIdeal ({opp}_{r} (O))$
6	3 5	eqtrid	$⊢ φ \to LIdeal (R) \cap LIdeal (O) = LIdeal (O) \cap LIdeal ({opp}_{r} (O))$
7		eqid	$⊢ LIdeal (R) = LIdeal (R)$
8		eqid	$⊢ LIdeal (O) = LIdeal (O)$
9		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
10	7 1 8 9	2idlval	$⊢ 2Ideal (R) = LIdeal (R) \cap LIdeal (O)$
11		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
12		eqid	$⊢ LIdeal ({opp}_{r} (O)) = LIdeal ({opp}_{r} (O))$
13		eqid	$⊢ 2Ideal (O) = 2Ideal (O)$
14	8 11 12 13	2idlval	$⊢ 2Ideal (O) = LIdeal (O) \cap LIdeal ({opp}_{r} (O))$
15	6 10 14	3eqtr4g	$⊢ φ \to 2Ideal (R) = 2Ideal (O)$

Metamath Proof Explorer