qsdrnglem2

	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)$
	qsdrnglem2.1	$⊢ B = {Base}_{R}$
	qsdrnglem2.q	$⊢ φ \to Q \in DivRing$
	qsdrnglem2.j	$⊢ φ \to J \in LIdeal (R)$
	qsdrnglem2.m	$⊢ φ \to M \subseteq J$
	qsdrnglem2.x	$⊢ φ \to X \in (J ∖ M)$
Assertion	qsdrnglem2	$⊢ φ \to J = B$

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		qsdrnglem2.1	$⊢ B = {Base}_{R}$
6		qsdrnglem2.q	$⊢ φ \to Q \in DivRing$
7		qsdrnglem2.j	$⊢ φ \to J \in LIdeal (R)$
8		qsdrnglem2.m	$⊢ φ \to M \subseteq J$
9		qsdrnglem2.x	$⊢ φ \to X \in (J ∖ M)$
10		nzrring	$⊢ R \in NzRing \to R \in Ring$
11	3 10	syl	$⊢ φ \to R \in Ring$
12	11	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to R \in Ring$
13	7	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to J \in LIdeal (R)$
14	12	ringgrpd	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to R \in Grp$
15		eqid	$⊢ LIdeal (R) = LIdeal (R)$
16	5 15	lidlss	$⊢ J \in LIdeal (R) \to J \subseteq B$
17	13 16	syl	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to J \subseteq B$
18		simplr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to s \in B$
19	9	eldifad	$⊢ φ \to X \in J$
20	19	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to X \in J$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22	15 5 21	lidlmcl	$⊢ ((R \in Ring \land J \in LIdeal (R)) \land (s \in B \land X \in J)) \to s \cdot_{R} X \in J$
23	12 13 18 20 22	syl22anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to s \cdot_{R} X \in J$
24	17 23	sseldd	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to s \cdot_{R} X \in B$
25		eqid	$⊢ 1_{R} = 1_{R}$
26	5 25	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
27	12 26	syl	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to 1_{R} \in B$
28		eqid	$⊢ +_{R} = +_{R}$
29		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
30	5 28 29	grpasscan1	$⊢ (R \in Grp \land s \cdot_{R} X \in B \land 1_{R} \in B) \to (s \cdot_{R} X) +_{R} ({inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R}) = 1_{R}$
31	14 24 27 30	syl3anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to (s \cdot_{R} X) +_{R} ({inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R}) = 1_{R}$
32	8	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to M \subseteq J$
33	7 16	syl	$⊢ φ \to J \subseteq B$
34	8 33	sstrd	$⊢ φ \to M \subseteq B$
35	34	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to M \subseteq B$
36		simpr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)$
37	36	oveq1d	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to {inv}_{r} (Q) ([X] (R ~_{QG} M)) \cdot_{Q} [X] (R ~_{QG} M) = [s] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M)$
38		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
39		eqid	$⊢ 0_{Q} = 0_{Q}$
40		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
41		eqid	$⊢ 1_{Q} = 1_{Q}$
42		eqid	$⊢ {inv}_{r} (Q) = {inv}_{r} (Q)$
43	6	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to Q \in DivRing$
44	33 19	sseldd	$⊢ φ \to X \in B$
45		ovex	$⊢ R ~_{QG} M \in V$
46	45	ecelqsi	$⊢ X \in B \to [X] (R ~_{QG} M) \in (B / (R ~_{QG} M))$
47	44 46	syl	$⊢ φ \to [X] (R ~_{QG} M) \in (B / (R ~_{QG} M))$
48	2	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} M)$
49	5	a1i	$⊢ φ \to B = {Base}_{R}$
50	45	a1i	$⊢ φ \to R ~_{QG} M \in V$
51	48 49 50 3	qusbas	$⊢ φ \to B / (R ~_{QG} M) = {Base}_{Q}$
52	47 51	eleqtrd	$⊢ φ \to [X] (R ~_{QG} M) \in {Base}_{Q}$
53	52	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [X] (R ~_{QG} M) \in {Base}_{Q}$
54	4	2idllidld	$⊢ φ \to M \in LIdeal (R)$
55	15	lidlsubg	$⊢ (R \in Ring \land M \in LIdeal (R)) \to M \in SubGrp (R)$
56	11 54 55	syl2anc	$⊢ φ \to M \in SubGrp (R)$
57		eqid	$⊢ R ~_{QG} M = R ~_{QG} M$
58	5 57	eqger	$⊢ M \in SubGrp (R) \to (R ~_{QG} M) Er B$
59	56 58	syl	$⊢ φ \to (R ~_{QG} M) Er B$
60		ecref	$⊢ ((R ~_{QG} M) Er B \land X \in B) \to X \in [X] (R ~_{QG} M)$
61	59 44 60	syl2anc	$⊢ φ \to X \in [X] (R ~_{QG} M)$
62	9	eldifbd	$⊢ φ \to \neg X \in M$
63		nelne1	$⊢ (X \in [X] (R ~_{QG} M) \land \neg X \in M) \to [X] (R ~_{QG} M) \neq M$
64	61 62 63	syl2anc	$⊢ φ \to [X] (R ~_{QG} M) \neq M$
65		lidlnsg	$⊢ (R \in Ring \land M \in LIdeal (R)) \to M \in NrmSGrp (R)$
66	11 54 65	syl2anc	$⊢ φ \to M \in NrmSGrp (R)$
67	2	qus0g	$⊢ M \in NrmSGrp (R) \to 0_{Q} = M$
68	66 67	syl	$⊢ φ \to 0_{Q} = M$
69	64 68	neeqtrrd	$⊢ φ \to [X] (R ~_{QG} M) \neq 0_{Q}$
70	69	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [X] (R ~_{QG} M) \neq 0_{Q}$
71	38 39 40 41 42 43 53 70	drnginvrld	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to {inv}_{r} (Q) ([X] (R ~_{QG} M)) \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q}$
72	4	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to M \in 2Ideal (R)$
73	44	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to X \in B$
74	2 5 21 40 12 72 18 73	qusmul2idl	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [s] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = [(s \cdot_{R} X)] (R ~_{QG} M)$
75	37 71 74	3eqtr3rd	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [(s \cdot_{R} X)] (R ~_{QG} M) = 1_{Q}$
76		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
77	2 76 25	qus1	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to (Q \in Ring \land [1_{R}] (R ~_{QG} M) = 1_{Q})$
78	77	simprd	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to [1_{R}] (R ~_{QG} M) = 1_{Q}$
79	12 72 78	syl2anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [1_{R}] (R ~_{QG} M) = 1_{Q}$
80	75 79	eqtr4d	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to [(s \cdot_{R} X)] (R ~_{QG} M) = [1_{R}] (R ~_{QG} M)$
81	56	ad2antrr	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to M \in SubGrp (R)$
82	81 58	syl	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to (R ~_{QG} M) Er B$
83	82 27	erth2	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to ((s \cdot_{R} X) (R ~_{QG} M) 1_{R} \leftrightarrow [(s \cdot_{R} X)] (R ~_{QG} M) = [1_{R}] (R ~_{QG} M))$
84	80 83	mpbird	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to (s \cdot_{R} X) (R ~_{QG} M) 1_{R}$
85	5 29 28 57	eqgval	$⊢ (R \in Ring \land M \subseteq B) \to ((s \cdot_{R} X) (R ~_{QG} M) 1_{R} \leftrightarrow (s \cdot_{R} X \in B \land 1_{R} \in B \land {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in M))$
86	85	biimpa	$⊢ ((R \in Ring \land M \subseteq B) \land (s \cdot_{R} X) (R ~_{QG} M) 1_{R}) \to (s \cdot_{R} X \in B \land 1_{R} \in B \land {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in M)$
87	86	simp3d	$⊢ ((R \in Ring \land M \subseteq B) \land (s \cdot_{R} X) (R ~_{QG} M) 1_{R}) \to {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in M$
88	12 35 84 87	syl21anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in M$
89	32 88	sseldd	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in J$
90	15 28	lidlacl	$⊢ ((R \in Ring \land J \in LIdeal (R)) \land (s \cdot_{R} X \in J \land {inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R} \in J)) \to (s \cdot_{R} X) +_{R} ({inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R}) \in J$
91	12 13 23 89 90	syl22anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to (s \cdot_{R} X) +_{R} ({inv}_{g} (R) (s \cdot_{R} X) +_{R} 1_{R}) \in J$
92	31 91	eqeltrrd	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to 1_{R} \in J$
93	15 5 25	lidl1el	$⊢ (R \in Ring \land J \in LIdeal (R)) \to (1_{R} \in J \leftrightarrow J = B)$
94	93	biimpa	$⊢ ((R \in Ring \land J \in LIdeal (R)) \land 1_{R} \in J) \to J = B$
95	12 13 92 94	syl21anc	$⊢ ((φ \land s \in B) \land {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)) \to J = B$
96	38 39 42 6 52 69	drnginvrcld	$⊢ φ \to {inv}_{r} (Q) ([X] (R ~_{QG} M)) \in {Base}_{Q}$
97	96 51	eleqtrrd	$⊢ φ \to {inv}_{r} (Q) ([X] (R ~_{QG} M)) \in (B / (R ~_{QG} M))$
98		elqsi	$⊢ {inv}_{r} (Q) ([X] (R ~_{QG} M)) \in (B / (R ~_{QG} M)) \to \exists s \in B {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)$
99	97 98	syl	$⊢ φ \to \exists s \in B {inv}_{r} (Q) ([X] (R ~_{QG} M)) = [s] (R ~_{QG} M)$
100	95 99	r19.29a	$⊢ φ \to J = B$

Metamath Proof Explorer

Theorem qsdrnglem2

Proof