opprmxidlabs

Description: The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypotheses	oppreqg.o	$⊢ O = {opp}_{r} (R)$
	oppr2idl.2	$⊢ φ \to R \in Ring$
	opprmxidl.3	$⊢ φ \to M \in MaxIdeal (R)$
Assertion	opprmxidlabs	$⊢ φ \to M \in MaxIdeal ({opp}_{r} (O))$

Proof

Step	Hyp	Ref	Expression
1		oppreqg.o	$⊢ O = {opp}_{r} (R)$
2		oppr2idl.2	$⊢ φ \to R \in Ring$
3		opprmxidl.3	$⊢ φ \to M \in MaxIdeal (R)$
4	1	opprring	$⊢ R \in Ring \to O \in Ring$
5		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
6	5	opprring	$⊢ O \in Ring \to {opp}_{r} (O) \in Ring$
7	2 4 6	3syl	$⊢ φ \to {opp}_{r} (O) \in Ring$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8	mxidlidl	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
10	2 3 9	syl2anc	$⊢ φ \to M \in LIdeal (R)$
11	1 2	opprlidlabs	$⊢ φ \to LIdeal (R) = LIdeal ({opp}_{r} (O))$
12	10 11	eleqtrd	$⊢ φ \to M \in LIdeal ({opp}_{r} (O))$
13	8	mxidlnr	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \neq {Base}_{R}$
14	2 3 13	syl2anc	$⊢ φ \to M \neq {Base}_{R}$
15	2	ad2antrr	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to R \in Ring$
16	3	ad2antrr	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to M \in MaxIdeal (R)$
17		simplr	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to j \in LIdeal ({opp}_{r} (O))$
18	11	ad2antrr	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to LIdeal (R) = LIdeal ({opp}_{r} (O))$
19	17 18	eleqtrrd	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to j \in LIdeal (R)$
20		simpr	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to M \subseteq j$
21	8	mxidlmax	$⊢ ((R \in Ring \land M \in MaxIdeal (R)) \land (j \in LIdeal (R) \land M \subseteq j)) \to (j = M \lor j = {Base}_{R})$
22	15 16 19 20 21	syl22anc	$⊢ ((φ \land j \in LIdeal ({opp}_{r} (O))) \land M \subseteq j) \to (j = M \lor j = {Base}_{R})$
23	22	ex	$⊢ (φ \land j \in LIdeal ({opp}_{r} (O))) \to (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
24	23	ralrimiva	$⊢ φ \to \forall j \in LIdeal ({opp}_{r} (O)) (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
25	1 8	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
26	5 25	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (O)}$
27	26	ismxidl	$⊢ {opp}_{r} (O) \in Ring \to (M \in MaxIdeal ({opp}_{r} (O)) \leftrightarrow (M \in LIdeal ({opp}_{r} (O)) \land M \neq {Base}_{R} \land \forall j \in LIdeal ({opp}_{r} (O)) (M \subseteq j \to (j = M \lor j = {Base}_{R}))))$
28	27	biimpar	$⊢ ({opp}_{r} (O) \in Ring \land (M \in LIdeal ({opp}_{r} (O)) \land M \neq {Base}_{R} \land \forall j \in LIdeal ({opp}_{r} (O)) (M \subseteq j \to (j = M \lor j = {Base}_{R})))) \to M \in MaxIdeal ({opp}_{r} (O))$
29	7 12 14 24 28	syl13anc	$⊢ φ \to M \in MaxIdeal ({opp}_{r} (O))$

Metamath Proof Explorer

Theorem opprmxidlabs

Proof