qsdrng

Description: An ideal M is both left and right maximal if and only if the factor ring Q is a division ring. (Contributed by Thierry Arnoux, 13-Mar-2025)

	Ref	Expression
Hypotheses	qsdrng.0	$⊢ O = {opp}_{r} (R)$
	qsdrng.q	$⊢ Q = R /_{𝑠} (R ~_{QG} M)$
	qsdrng.r	$⊢ φ \to R \in NzRing$
	qsdrng.2	$⊢ φ \to M \in 2Ideal (R)$
Assertion	qsdrng	Could not format assertion : No typesetting found for \|- ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		qsdrng.0	$⊢ O = {opp}_{r} (R)$
2		qsdrng.q	$⊢ Q = R /_{𝑠} (R ~_{QG} M)$
3		qsdrng.r	$⊢ φ \to R \in NzRing$
4		qsdrng.2	$⊢ φ \to M \in 2Ideal (R)$
5		nzrring	$⊢ R \in NzRing \to R \in Ring$
6	3 5	syl	$⊢ φ \to R \in Ring$
7	6	adantr	$⊢ (φ \land Q \in DivRing) \to R \in Ring$
8	4	2idllidld	$⊢ φ \to M \in LIdeal (R)$
9	8	adantr	$⊢ (φ \land Q \in DivRing) \to M \in LIdeal (R)$
10		drngnzr	$⊢ Q \in DivRing \to Q \in NzRing$
11	10	ad2antlr	$⊢ ((φ \land Q \in DivRing) \land M = {Base}_{R}) \to Q \in NzRing$
12		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
13	2 12	qusring	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to Q \in Ring$
14	6 4 13	syl2anc	$⊢ φ \to Q \in Ring$
15	14	adantr	$⊢ (φ \land M = {Base}_{R}) \to Q \in Ring$
16		oveq2	$⊢ M = {Base}_{R} \to R ~_{QG} M = R ~_{QG} {Base}_{R}$
17	16	oveq2d	$⊢ M = {Base}_{R} \to R /_{𝑠} (R ~_{QG} M) = R /_{𝑠} (R ~_{QG} {Base}_{R})$
18	2 17	eqtrid	$⊢ M = {Base}_{R} \to Q = R /_{𝑠} (R ~_{QG} {Base}_{R})$
19	18	fveq2d	$⊢ M = {Base}_{R} \to {Base}_{Q} = {Base}_{(R /_{𝑠} (R ~_{QG} {Base}_{R}))}$
20	6	ringgrpd	$⊢ φ \to R \in Grp$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22		eqid	$⊢ R /_{𝑠} (R ~_{QG} {Base}_{R}) = R /_{𝑠} (R ~_{QG} {Base}_{R})$
23	21 22	qustriv	$⊢ R \in Grp \to {Base}_{(R /_{𝑠} (R ~_{QG} {Base}_{R}))} = \{{Base}_{R}\}$
24	20 23	syl	$⊢ φ \to {Base}_{(R /_{𝑠} (R ~_{QG} {Base}_{R}))} = \{{Base}_{R}\}$
25	19 24	sylan9eqr	$⊢ (φ \land M = {Base}_{R}) \to {Base}_{Q} = \{{Base}_{R}\}$
26	25	fveq2d	$⊢ (φ \land M = {Base}_{R}) \to \|{Base}_{Q}\| = \|\{{Base}_{R}\}\|$
27		fvex	$⊢ {Base}_{R} \in V$
28		hashsng	$⊢ {Base}_{R} \in V \to \|\{{Base}_{R}\}\| = 1$
29	27 28	ax-mp	$⊢ \|\{{Base}_{R}\}\| = 1$
30	26 29	eqtrdi	$⊢ (φ \land M = {Base}_{R}) \to \|{Base}_{Q}\| = 1$
31		0ringnnzr	$⊢ Q \in Ring \to (\|{Base}_{Q}\| = 1 \leftrightarrow \neg Q \in NzRing)$
32	31	biimpa	$⊢ (Q \in Ring \land \|{Base}_{Q}\| = 1) \to \neg Q \in NzRing$
33	15 30 32	syl2anc	$⊢ (φ \land M = {Base}_{R}) \to \neg Q \in NzRing$
34	33	adantlr	$⊢ ((φ \land Q \in DivRing) \land M = {Base}_{R}) \to \neg Q \in NzRing$
35	11 34	pm2.65da	$⊢ (φ \land Q \in DivRing) \to \neg M = {Base}_{R}$
36	35	neqned	$⊢ (φ \land Q \in DivRing) \to M \neq {Base}_{R}$
37		simplr	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to M \subseteq j$
38		simpr	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to \neg j = M$
39	38	neqned	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to j \neq M$
40	39	necomd	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to M \neq j$
41		pssdifn0	$⊢ (M \subseteq j \land M \neq j) \to j ∖ M \neq \emptyset$
42	37 40 41	syl2anc	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to j ∖ M \neq \emptyset$
43		n0	$⊢ j ∖ M \neq \emptyset \leftrightarrow \exists x x \in (j ∖ M)$
44	42 43	sylib	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to \exists x x \in (j ∖ M)$
45	3	ad5antr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to R \in NzRing$
46	4	ad5antr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to M \in 2Ideal (R)$
47		simp-5r	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to Q \in DivRing$
48		simp-4r	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to j \in LIdeal (R)$
49	37	adantr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to M \subseteq j$
50		simpr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to x \in (j ∖ M)$
51	1 2 45 46 21 47 48 49 50	qsdrnglem2	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to j = {Base}_{R}$
52	44 51	exlimddv	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \land \neg j = M) \to j = {Base}_{R}$
53	52	ex	$⊢ (((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \to (\neg j = M \to j = {Base}_{R})$
54	53	orrd	$⊢ (((φ \land Q \in DivRing) \land j \in LIdeal (R)) \land M \subseteq j) \to (j = M \lor j = {Base}_{R})$
55	54	ex	$⊢ ((φ \land Q \in DivRing) \land j \in LIdeal (R)) \to (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
56	55	ralrimiva	$⊢ (φ \land Q \in DivRing) \to \forall j \in LIdeal (R) (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
57	21	ismxidl	Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) : No typesetting found for \|- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) with typecode \|-
58	57	biimpar	Could not format ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ ( M e. ( LIdeal ` R ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` R ) ) with typecode \|-
59	7 9 36 56 58	syl13anc	Could not format ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` R ) ) with typecode \|-
60	1	opprring	$⊢ R \in Ring \to O \in Ring$
61	6 60	syl	$⊢ φ \to O \in Ring$
62	61	adantr	$⊢ (φ \land Q \in DivRing) \to O \in Ring$
63	4	adantr	$⊢ (φ \land Q \in DivRing) \to M \in 2Ideal (R)$
64	63 1	2idlridld	$⊢ (φ \land Q \in DivRing) \to M \in LIdeal (O)$
65		simplr	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to M \subseteq j$
66		simpr	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to \neg j = M$
67	66	neqned	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to j \neq M$
68	67	necomd	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to M \neq j$
69	65 68 41	syl2anc	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to j ∖ M \neq \emptyset$
70	69 43	sylib	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to \exists x x \in (j ∖ M)$
71		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
72		eqid	$⊢ O /_{𝑠} (O ~_{QG} M) = O /_{𝑠} (O ~_{QG} M)$
73	1	opprnzr	$⊢ R \in NzRing \to O \in NzRing$
74	3 73	syl	$⊢ φ \to O \in NzRing$
75	74	ad5antr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to O \in NzRing$
76	1 6	oppr2idl	$⊢ φ \to 2Ideal (R) = 2Ideal (O)$
77	4 76	eleqtrd	$⊢ φ \to M \in 2Ideal (O)$
78	77	ad5antr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to M \in 2Ideal (O)$
79	1 21	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
80		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
81	80	opprdrng	$⊢ Q \in DivRing \leftrightarrow {opp}_{r} (Q) \in DivRing$
82	21 1 2 6 4	opprqusdrng	$⊢ φ \to ({opp}_{r} (Q) \in DivRing \leftrightarrow O /_{𝑠} (O ~_{QG} M) \in DivRing)$
83	82	biimpa	$⊢ (φ \land {opp}_{r} (Q) \in DivRing) \to O /_{𝑠} (O ~_{QG} M) \in DivRing$
84	81 83	sylan2b	$⊢ (φ \land Q \in DivRing) \to O /_{𝑠} (O ~_{QG} M) \in DivRing$
85	84	ad4antr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to O /_{𝑠} (O ~_{QG} M) \in DivRing$
86		simp-4r	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to j \in LIdeal (O)$
87	65	adantr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to M \subseteq j$
88		simpr	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to x \in (j ∖ M)$
89	71 72 75 78 79 85 86 87 88	qsdrnglem2	$⊢ (((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \land x \in (j ∖ M)) \to j = {Base}_{R}$
90	70 89	exlimddv	$⊢ ((((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \land \neg j = M) \to j = {Base}_{R}$
91	90	ex	$⊢ (((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \to (\neg j = M \to j = {Base}_{R})$
92	91	orrd	$⊢ (((φ \land Q \in DivRing) \land j \in LIdeal (O)) \land M \subseteq j) \to (j = M \lor j = {Base}_{R})$
93	92	ex	$⊢ ((φ \land Q \in DivRing) \land j \in LIdeal (O)) \to (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
94	93	ralrimiva	$⊢ (φ \land Q \in DivRing) \to \forall j \in LIdeal (O) (M \subseteq j \to (j = M \lor j = {Base}_{R}))$
95	79	ismxidl	Could not format ( O e. Ring -> ( M e. ( MaxIdeal ` O ) <-> ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) : No typesetting found for \|- ( O e. Ring -> ( M e. ( MaxIdeal ` O ) <-> ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) ) with typecode \|-
96	95	biimpar	Could not format ( ( O e. Ring /\ ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` O ) ) : No typesetting found for \|- ( ( O e. Ring /\ ( M e. ( LIdeal ` O ) /\ M =/= ( Base ` R ) /\ A. j e. ( LIdeal ` O ) ( M C_ j -> ( j = M \/ j = ( Base ` R ) ) ) ) ) -> M e. ( MaxIdeal ` O ) ) with typecode \|-
97	62 64 36 94 96	syl13anc	Could not format ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` O ) ) : No typesetting found for \|- ( ( ph /\ Q e. DivRing ) -> M e. ( MaxIdeal ` O ) ) with typecode \|-
98	59 97	jca	Could not format ( ( ph /\ Q e. DivRing ) -> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) : No typesetting found for \|- ( ( ph /\ Q e. DivRing ) -> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) with typecode \|-
99	3	adantr	Could not format ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> R e. NzRing ) : No typesetting found for \|- ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> R e. NzRing ) with typecode \|-
100		simprl	Could not format ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` R ) ) with typecode \|-
101		simprr	Could not format ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` O ) ) : No typesetting found for \|- ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> M e. ( MaxIdeal ` O ) ) with typecode \|-
102	1 2 99 100 101	qsdrngi	Could not format ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> Q e. DivRing ) : No typesetting found for \|- ( ( ph /\ ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) -> Q e. DivRing ) with typecode \|-
103	98 102	impbida	Could not format ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) ) : No typesetting found for \|- ( ph -> ( Q e. DivRing <-> ( M e. ( MaxIdeal ` R ) /\ M e. ( MaxIdeal ` O ) ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem qsdrng

Proof