qsdrngi

Description: A quotient by a maximal left and maximal right ideal is a division ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

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

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		qsdrngi.1	Could not format ( ph -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ph -> M e. ( MaxIdeal ` R ) ) with typecode \|-
5		qsdrngi.2	Could not format ( ph -> M e. ( MaxIdeal ` O ) ) : No typesetting found for \|- ( ph -> M e. ( MaxIdeal ` O ) ) with typecode \|-
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		nzrring	$⊢ R \in NzRing \to R \in Ring$
8	3 7	syl	$⊢ φ \to R \in Ring$
9	6	mxidlidl	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode \|-
10	8 4 9	syl2anc	$⊢ φ \to M \in LIdeal (R)$
11	1	opprring	$⊢ R \in Ring \to O \in Ring$
12	8 11	syl	$⊢ φ \to O \in Ring$
13		eqid	$⊢ {Base}_{O} = {Base}_{O}$
14	13	mxidlidl	Could not format ( ( O e. Ring /\ M e. ( MaxIdeal ` O ) ) -> M e. ( LIdeal ` O ) ) : No typesetting found for \|- ( ( O e. Ring /\ M e. ( MaxIdeal ` O ) ) -> M e. ( LIdeal ` O ) ) with typecode \|-
15	12 5 14	syl2anc	$⊢ φ \to M \in LIdeal (O)$
16	10 15	elind	$⊢ φ \to M \in (LIdeal (R) \cap LIdeal (O))$
17		eqid	$⊢ LIdeal (R) = LIdeal (R)$
18		eqid	$⊢ LIdeal (O) = LIdeal (O)$
19		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
20	17 1 18 19	2idlval	$⊢ 2Ideal (R) = LIdeal (R) \cap LIdeal (O)$
21	16 20	eleqtrrdi	$⊢ φ \to M \in 2Ideal (R)$
22	6	mxidlnr	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= ( Base ` R ) ) with typecode \|-
23	8 4 22	syl2anc	$⊢ φ \to M \neq {Base}_{R}$
24	2 6 8 3 21 23	qsnzr	$⊢ φ \to Q \in NzRing$
25		eqid	$⊢ 1_{Q} = 1_{Q}$
26		eqid	$⊢ 0_{Q} = 0_{Q}$
27	25 26	nzrnz	$⊢ Q \in NzRing \to 1_{Q} \neq 0_{Q}$
28	24 27	syl	$⊢ φ \to 1_{Q} \neq 0_{Q}$
29		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
30		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
31		eqid	$⊢ Unit (Q) = Unit (Q)$
32	2 19	qusring	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to Q \in Ring$
33	8 21 32	syl2anc	$⊢ φ \to Q \in Ring$
34	33	ad10antr	$⊢ ((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \to Q \in Ring$
35	34	adantr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to Q \in Ring$
36		eldifi	$⊢ u \in ({Base}_{Q} ∖ \{0_{Q}\}) \to u \in {Base}_{Q}$
37	36	adantl	$⊢ (φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \to u \in {Base}_{Q}$
38	37	ad10antr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u \in {Base}_{Q}$
39		ovex	$⊢ R ~_{QG} M \in V$
40	39	ecelqsi	$⊢ r \in {Base}_{R} \to [r] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
41	40	ad4antlr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [r] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
42	2	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} M)$
43		eqidd	$⊢ φ \to {Base}_{R} = {Base}_{R}$
44		ovexd	$⊢ φ \to R ~_{QG} M \in V$
45	42 43 44 3	qusbas	$⊢ φ \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
46	45	adantr	$⊢ (φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
47	46	ad10antr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
48	41 47	eleqtrd	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [r] (R ~_{QG} M) \in {Base}_{Q}$
49	39	ecelqsi	$⊢ s \in {Base}_{R} \to [s] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
50	49	ad2antlr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
51	50 47	eleqtrd	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \in {Base}_{Q}$
52		simpllr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to v = [r] (R ~_{QG} M)$
53		simp-9r	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u = [x] (R ~_{QG} M)$
54	53	eqcomd	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [x] (R ~_{QG} M) = u$
55	52 54	oveq12d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to v \cdot_{Q} [x] (R ~_{QG} M) = [r] (R ~_{QG} M) \cdot_{Q} u$
56		simp-7r	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}$
57	55 56	eqtr3d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [r] (R ~_{QG} M) \cdot_{Q} u = 1_{Q}$
58		eqid	$⊢ {opp}_{r} (Q) = {opp}_{r} (Q)$
59		eqid	$⊢ \cdot_{{opp}_{r} (Q)} = \cdot_{{opp}_{r} (Q)}$
60	29 30 58 59	opprmul	$⊢ [s] (R ~_{QG} M) \cdot_{{opp}_{r} (Q)} u = u \cdot_{Q} [s] (R ~_{QG} M)$
61		simp-5r	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}$
62	8	ad3antrrr	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to R \in Ring$
63	62	ad8antr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to R \in Ring$
64	21	ad3antrrr	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to M \in 2Ideal (R)$
65	64	ad8antr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to M \in 2Ideal (R)$
66	6 1 2 63 65 29 51 38	opprqusmulr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \cdot_{{opp}_{r} (Q)} u = [s] (R ~_{QG} M) \cdot_{(O /_{𝑠} (O ~_{QG} M))} u$
67		simpr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to w = [s] (R ~_{QG} M)$
68	6 17	lidlss	$⊢ M \in LIdeal (R) \to M \subseteq {Base}_{R}$
69	10 68	syl	$⊢ φ \to M \subseteq {Base}_{R}$
70	1 6	oppreqg	$⊢ (R \in Ring \land M \subseteq {Base}_{R}) \to R ~_{QG} M = O ~_{QG} M$
71	8 69 70	syl2anc	$⊢ φ \to R ~_{QG} M = O ~_{QG} M$
72	71	ad10antr	$⊢ ((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \to R ~_{QG} M = O ~_{QG} M$
73	72	adantr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to R ~_{QG} M = O ~_{QG} M$
74	73	eceq2d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [x] (R ~_{QG} M) = [x] (O ~_{QG} M)$
75	53 74	eqtr2d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [x] (O ~_{QG} M) = u$
76	67 75	oveq12d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = [s] (R ~_{QG} M) \cdot_{(O /_{𝑠} (O ~_{QG} M))} u$
77	66 76	eqtr4d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \cdot_{{opp}_{r} (Q)} u = w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M)$
78	58 25	oppr1	$⊢ 1_{Q} = 1_{{opp}_{r} (Q)}$
79	6 1 2 8 21	opprqus1r	$⊢ φ \to 1_{{opp}_{r} (Q)} = 1_{(O /_{𝑠} (O ~_{QG} M))}$
80	78 79	eqtrid	$⊢ φ \to 1_{Q} = 1_{(O /_{𝑠} (O ~_{QG} M))}$
81	80	ad10antr	$⊢ ((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \to 1_{Q} = 1_{(O /_{𝑠} (O ~_{QG} M))}$
82	81	adantr	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to 1_{Q} = 1_{(O /_{𝑠} (O ~_{QG} M))}$
83	61 77 82	3eqtr4d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \cdot_{{opp}_{r} (Q)} u = 1_{Q}$
84	60 83	eqtr3id	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u \cdot_{Q} [s] (R ~_{QG} M) = 1_{Q}$
85	29 26 25 30 31 35 38 48 51 57 84	ringinveu	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) = [r] (R ~_{QG} M)$
86	85 67 52	3eqtr4rd	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to v = w$
87	86	oveq2d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u \cdot_{Q} v = u \cdot_{Q} w$
88	67	oveq2d	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u \cdot_{Q} w = u \cdot_{Q} [s] (R ~_{QG} M)$
89	87 88 84	3eqtrd	$⊢ (((((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \land s \in {Base}_{R}) \land w = [s] (R ~_{QG} M)) \to u \cdot_{Q} v = 1_{Q}$
90		simp-4r	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}$
91	71	qseq2d	$⊢ φ \to {Base}_{R} / (R ~_{QG} M) = {Base}_{R} / (O ~_{QG} M)$
92	91	ad9antr	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to {Base}_{R} / (R ~_{QG} M) = {Base}_{R} / (O ~_{QG} M)$
93		eqidd	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to O /_{𝑠} (O ~_{QG} M) = O /_{𝑠} (O ~_{QG} M)$
94	1 6	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
95	94	a1i	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to {Base}_{R} = {Base}_{O}$
96		ovexd	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to O ~_{QG} M \in V$
97	1	fvexi	$⊢ O \in V$
98	97	a1i	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to O \in V$
99	93 95 96 98	qusbas	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to {Base}_{R} / (O ~_{QG} M) = {Base}_{(O /_{𝑠} (O ~_{QG} M))}$
100	92 99	eqtr2d	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to {Base}_{(O /_{𝑠} (O ~_{QG} M))} = {Base}_{R} / (R ~_{QG} M)$
101	90 100	eleqtrd	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to w \in ({Base}_{R} / (R ~_{QG} M))$
102		elqsi	$⊢ w \in ({Base}_{R} / (R ~_{QG} M)) \to \exists s \in {Base}_{R} w = [s] (R ~_{QG} M)$
103	101 102	syl	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to \exists s \in {Base}_{R} w = [s] (R ~_{QG} M)$
104	89 103	r19.29a	$⊢ (((((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \land r \in {Base}_{R}) \land v = [r] (R ~_{QG} M)) \to u \cdot_{Q} v = 1_{Q}$
105		simp-4r	$⊢ (((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \to v \in {Base}_{Q}$
106	46	ad6antr	$⊢ (((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
107	105 106	eleqtrrd	$⊢ (((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \to v \in ({Base}_{R} / (R ~_{QG} M))$
108		elqsi	$⊢ v \in ({Base}_{R} / (R ~_{QG} M)) \to \exists r \in {Base}_{R} v = [r] (R ~_{QG} M)$
109	107 108	syl	$⊢ (((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \to \exists r \in {Base}_{R} v = [r] (R ~_{QG} M)$
110	104 109	r19.29a	$⊢ (((((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \land w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))}) \land w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}) \to u \cdot_{Q} v = 1_{Q}$
111		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
112		eqid	$⊢ O /_{𝑠} (O ~_{QG} M) = O /_{𝑠} (O ~_{QG} M)$
113	3	ad3antrrr	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to R \in NzRing$
114	1	opprnzr	$⊢ R \in NzRing \to O \in NzRing$
115	113 114	syl	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to O \in NzRing$
116	5	ad3antrrr	Could not format ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` O ) ) : No typesetting found for \|- ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` O ) ) with typecode \|-
117	4	ad3antrrr	Could not format ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` R ) ) with typecode \|-
118	1 62 117	opprmxidlabs	Could not format ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` ( oppR ` O ) ) ) : No typesetting found for \|- ( ( ( ( ph /\ u e. ( ( Base ` Q ) \ { ( 0g ` Q ) } ) ) /\ x e. ( Base ` R ) ) /\ u = [ x ] ( R ~QG M ) ) -> M e. ( MaxIdeal ` ( oppR ` O ) ) ) with typecode \|-
119		simplr	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to x \in {Base}_{R}$
120	94	a1i	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to {Base}_{R} = {Base}_{O}$
121	119 120	eleqtrd	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to x \in {Base}_{O}$
122		simplr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to u = [x] (R ~_{QG} M)$
123	8	ringgrpd	$⊢ φ \to R \in Grp$
124	123	ad4antr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to R \in Grp$
125		lidlnsg	$⊢ (R \in Ring \land M \in LIdeal (R)) \to M \in NrmSGrp (R)$
126	8 10 125	syl2anc	$⊢ φ \to M \in NrmSGrp (R)$
127		nsgsubg	$⊢ M \in NrmSGrp (R) \to M \in SubGrp (R)$
128	126 127	syl	$⊢ φ \to M \in SubGrp (R)$
129	128	ad4antr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to M \in SubGrp (R)$
130		simpr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to x \in M$
131		eqid	$⊢ R ~_{QG} M = R ~_{QG} M$
132	131	eqg0el	$⊢ (R \in Grp \land M \in SubGrp (R)) \to ([x] (R ~_{QG} M) = M \leftrightarrow x \in M)$
133	132	biimpar	$⊢ ((R \in Grp \land M \in SubGrp (R)) \land x \in M) \to [x] (R ~_{QG} M) = M$
134	124 129 130 133	syl21anc	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to [x] (R ~_{QG} M) = M$
135		eqid	$⊢ 0_{R} = 0_{R}$
136	6 131 135	eqgid	$⊢ M \in SubGrp (R) \to [0_{R}] (R ~_{QG} M) = M$
137	129 136	syl	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to [0_{R}] (R ~_{QG} M) = M$
138	134 137	eqtr4d	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to [x] (R ~_{QG} M) = [0_{R}] (R ~_{QG} M)$
139	2 135	qus0	$⊢ M \in NrmSGrp (R) \to [0_{R}] (R ~_{QG} M) = 0_{Q}$
140	126 139	syl	$⊢ φ \to [0_{R}] (R ~_{QG} M) = 0_{Q}$
141	140	ad4antr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to [0_{R}] (R ~_{QG} M) = 0_{Q}$
142	122 138 141	3eqtrd	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to u = 0_{Q}$
143		eldifsnneq	$⊢ u \in ({Base}_{Q} ∖ \{0_{Q}\}) \to \neg u = 0_{Q}$
144	143	ad4antlr	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land x \in M) \to \neg u = 0_{Q}$
145	142 144	pm2.65da	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to \neg x \in M$
146	111 112 115 116 118 121 145	qsdrngilem	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to \exists w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))} w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}$
147	146	ad2antrr	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to \exists w \in {Base}_{(O /_{𝑠} (O ~_{QG} M))} w \cdot_{(O /_{𝑠} (O ~_{QG} M))} [x] (O ~_{QG} M) = 1_{(O /_{𝑠} (O ~_{QG} M))}$
148	110 147	r19.29a	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to u \cdot_{Q} v = 1_{Q}$
149		simpllr	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to u = [x] (R ~_{QG} M)$
150	149	oveq2d	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to v \cdot_{Q} u = v \cdot_{Q} [x] (R ~_{QG} M)$
151		simpr	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}$
152	150 151	eqtrd	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to v \cdot_{Q} u = 1_{Q}$
153	148 152	jca	$⊢ (((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land v \in {Base}_{Q}) \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}) \to (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})$
154	153	anasss	$⊢ ((((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \land (v \in {Base}_{Q} \land v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q})) \to (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})$
155	1 2 113 117 116 119 145	qsdrngilem	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to \exists v \in {Base}_{Q} v \cdot_{Q} [x] (R ~_{QG} M) = 1_{Q}$
156	154 155	reximddv	$⊢ (((φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \land x \in {Base}_{R}) \land u = [x] (R ~_{QG} M)) \to \exists v \in {Base}_{Q} (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})$
157	37 46	eleqtrrd	$⊢ (φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \to u \in ({Base}_{R} / (R ~_{QG} M))$
158		elqsi	$⊢ u \in ({Base}_{R} / (R ~_{QG} M)) \to \exists x \in {Base}_{R} u = [x] (R ~_{QG} M)$
159	157 158	syl	$⊢ (φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \to \exists x \in {Base}_{R} u = [x] (R ~_{QG} M)$
160	156 159	r19.29a	$⊢ (φ \land u \in ({Base}_{Q} ∖ \{0_{Q}\})) \to \exists v \in {Base}_{Q} (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})$
161	160	ralrimiva	$⊢ φ \to \forall u \in ({Base}_{Q} ∖ \{0_{Q}\}) \exists v \in {Base}_{Q} (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})$
162	29 26 25 30 31 33	isdrng4	$⊢ φ \to (Q \in DivRing \leftrightarrow (1_{Q} \neq 0_{Q} \land \forall u \in ({Base}_{Q} ∖ \{0_{Q}\}) \exists v \in {Base}_{Q} (u \cdot_{Q} v = 1_{Q} \land v \cdot_{Q} u = 1_{Q})))$
163	28 161 162	mpbir2and	$⊢ φ \to Q \in DivRing$

Metamath Proof Explorer

Theorem qsdrngi

Proof