qsdrngilem

	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 \|-
	qsdrngilem.1	$⊢ φ \to X \in {Base}_{R}$
	qsdrngilem.2	$⊢ φ \to \neg X \in M$
Assertion	qsdrngilem	$⊢ φ \to \exists v \in {Base}_{Q} v \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q}$

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		qsdrngilem.1	$⊢ φ \to X \in {Base}_{R}$
7		qsdrngilem.2	$⊢ φ \to \neg X \in M$
8		simpllr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to r \in {Base}_{R}$
9		ovex	$⊢ R ~_{QG} M \in V$
10	9	ecelqsi	$⊢ r \in {Base}_{R} \to [r] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
11	8 10	syl	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [r] (R ~_{QG} M) \in ({Base}_{R} / (R ~_{QG} M))$
12	2	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} M)$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	13	a1i	$⊢ φ \to {Base}_{R} = {Base}_{R}$
15		ovexd	$⊢ φ \to R ~_{QG} M \in V$
16	12 14 15 3	qusbas	$⊢ φ \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
17	16	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {Base}_{R} / (R ~_{QG} M) = {Base}_{Q}$
18	11 17	eleqtrd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [r] (R ~_{QG} M) \in {Base}_{Q}$
19		oveq1	$⊢ v = [r] (R ~_{QG} M) \to v \cdot_{Q} [X] (R ~_{QG} M) = [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M)$
20	19	eqeq1d	$⊢ v = [r] (R ~_{QG} M) \to (v \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q} \leftrightarrow [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q})$
21	20	adantl	$⊢ ((((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \land v = [r] (R ~_{QG} M)) \to (v \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q} \leftrightarrow [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q})$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
24		nzrring	$⊢ R \in NzRing \to R \in Ring$
25	3 24	syl	$⊢ φ \to R \in Ring$
26	25	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to R \in Ring$
27	13	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 \|-
28	25 4 27	syl2anc	$⊢ φ \to M \in LIdeal (R)$
29	1	opprring	$⊢ R \in Ring \to O \in Ring$
30	25 29	syl	$⊢ φ \to O \in Ring$
31		eqid	$⊢ {Base}_{O} = {Base}_{O}$
32	31	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 \|-
33	30 5 32	syl2anc	$⊢ φ \to M \in LIdeal (O)$
34	28 33	elind	$⊢ φ \to M \in (LIdeal (R) \cap LIdeal (O))$
35		eqid	$⊢ LIdeal (R) = LIdeal (R)$
36		eqid	$⊢ LIdeal (O) = LIdeal (O)$
37		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
38	35 1 36 37	2idlval	$⊢ 2Ideal (R) = LIdeal (R) \cap LIdeal (O)$
39	34 38	eleqtrrdi	$⊢ φ \to M \in 2Ideal (R)$
40	39	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to M \in 2Ideal (R)$
41	6	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to X \in {Base}_{R}$
42	2 13 22 23 26 40 8 41	qusmul2	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = [(r \cdot_{R} X)] (R ~_{QG} M)$
43		lidlnsg	$⊢ (R \in Ring \land M \in LIdeal (R)) \to M \in NrmSGrp (R)$
44	25 28 43	syl2anc	$⊢ φ \to M \in NrmSGrp (R)$
45		nsgsubg	$⊢ M \in NrmSGrp (R) \to M \in SubGrp (R)$
46		eqid	$⊢ R ~_{QG} M = R ~_{QG} M$
47	13 46	eqger	$⊢ M \in SubGrp (R) \to (R ~_{QG} M) Er {Base}_{R}$
48	44 45 47	3syl	$⊢ φ \to (R ~_{QG} M) Er {Base}_{R}$
49	48	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to (R ~_{QG} M) Er {Base}_{R}$
50	13 35	lidlss	$⊢ M \in LIdeal (R) \to M \subseteq {Base}_{R}$
51	28 50	syl	$⊢ φ \to M \subseteq {Base}_{R}$
52	51	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to M \subseteq {Base}_{R}$
53	13 22 26 8 41	ringcld	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to r \cdot_{R} X \in {Base}_{R}$
54		eqid	$⊢ 1_{R} = 1_{R}$
55	13 54	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
56	25 55	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
57	56	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to 1_{R} \in {Base}_{R}$
58		simpr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to 1_{R} = (r \cdot_{R} X) +_{R} m$
59	58	oveq2d	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) +_{R} 1_{R} = {inv}_{g} (R) (r \cdot_{R} X) +_{R} ((r \cdot_{R} X) +_{R} m)$
60		eqid	$⊢ +_{R} = +_{R}$
61		eqid	$⊢ 0_{R} = 0_{R}$
62		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
63	25	ringgrpd	$⊢ φ \to R \in Grp$
64	63	ad3antrrr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to R \in Grp$
65	13 60 61 62 64 53	grplinvd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) +_{R} (r \cdot_{R} X) = 0_{R}$
66	65	oveq1d	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to ({inv}_{g} (R) (r \cdot_{R} X) +_{R} (r \cdot_{R} X)) +_{R} m = 0_{R} +_{R} m$
67	13 62 64 53	grpinvcld	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) \in {Base}_{R}$
68		simplr	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to m \in M$
69	52 68	sseldd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to m \in {Base}_{R}$
70	13 60 64 67 53 69	grpassd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to ({inv}_{g} (R) (r \cdot_{R} X) +_{R} (r \cdot_{R} X)) +_{R} m = {inv}_{g} (R) (r \cdot_{R} X) +_{R} ((r \cdot_{R} X) +_{R} m)$
71	13 60 61 64 69	grplidd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to 0_{R} +_{R} m = m$
72	66 70 71	3eqtr3d	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) +_{R} ((r \cdot_{R} X) +_{R} m) = m$
73	59 72	eqtrd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) +_{R} 1_{R} = m$
74	73 68	eqeltrd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to {inv}_{g} (R) (r \cdot_{R} X) +_{R} 1_{R} \in M$
75	13 62 60 46	eqgval	$⊢ (R \in Ring \land M \subseteq {Base}_{R}) \to ((r \cdot_{R} X) (R ~_{QG} M) 1_{R} \leftrightarrow (r \cdot_{R} X \in {Base}_{R} \land 1_{R} \in {Base}_{R} \land {inv}_{g} (R) (r \cdot_{R} X) +_{R} 1_{R} \in M))$
76	75	biimpar	$⊢ ((R \in Ring \land M \subseteq {Base}_{R}) \land (r \cdot_{R} X \in {Base}_{R} \land 1_{R} \in {Base}_{R} \land {inv}_{g} (R) (r \cdot_{R} X) +_{R} 1_{R} \in M)) \to (r \cdot_{R} X) (R ~_{QG} M) 1_{R}$
77	26 52 53 57 74 76	syl23anc	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to (r \cdot_{R} X) (R ~_{QG} M) 1_{R}$
78	49 77	erthi	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [(r \cdot_{R} X)] (R ~_{QG} M) = [1_{R}] (R ~_{QG} M)$
79	42 78	eqtrd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = [1_{R}] (R ~_{QG} M)$
80	2 37 54	qus1	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to (Q \in Ring \land [1_{R}] (R ~_{QG} M) = 1_{Q})$
81	80	simprd	$⊢ (R \in Ring \land M \in 2Ideal (R)) \to [1_{R}] (R ~_{QG} M) = 1_{Q}$
82	26 40 81	syl2anc	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [1_{R}] (R ~_{QG} M) = 1_{Q}$
83	79 82	eqtrd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to [r] (R ~_{QG} M) \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q}$
84	18 21 83	rspcedvd	$⊢ (((φ \land r \in {Base}_{R}) \land m \in M) \land 1_{R} = (r \cdot_{R} X) +_{R} m) \to \exists v \in {Base}_{Q} v \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q}$
85	6	snssd	$⊢ φ \to \{X\} \subseteq {Base}_{R}$
86	51 85	unssd	$⊢ φ \to M \cup \{X\} \subseteq {Base}_{R}$
87		eqid	$⊢ RSpan (R) = RSpan (R)$
88	87 13 35	rspcl	$⊢ (R \in Ring \land M \cup \{X\} \subseteq {Base}_{R}) \to RSpan (R) (M \cup \{X\}) \in LIdeal (R)$
89	25 86 88	syl2anc	$⊢ φ \to RSpan (R) (M \cup \{X\}) \in LIdeal (R)$
90	87 13	rspssid	$⊢ (R \in Ring \land M \cup \{X\} \subseteq {Base}_{R}) \to M \cup \{X\} \subseteq RSpan (R) (M \cup \{X\})$
91	25 86 90	syl2anc	$⊢ φ \to M \cup \{X\} \subseteq RSpan (R) (M \cup \{X\})$
92	91	unssad	$⊢ φ \to M \subseteq RSpan (R) (M \cup \{X\})$
93	91	unssbd	$⊢ φ \to \{X\} \subseteq RSpan (R) (M \cup \{X\})$
94		snssg	$⊢ X \in {Base}_{R} \to (X \in RSpan (R) (M \cup \{X\}) \leftrightarrow \{X\} \subseteq RSpan (R) (M \cup \{X\}))$
95	94	biimpar	$⊢ (X \in {Base}_{R} \land \{X\} \subseteq RSpan (R) (M \cup \{X\})) \to X \in RSpan (R) (M \cup \{X\})$
96	6 93 95	syl2anc	$⊢ φ \to X \in RSpan (R) (M \cup \{X\})$
97	96 7	eldifd	$⊢ φ \to X \in (RSpan (R) (M \cup \{X\}) ∖ M)$
98	13 25 4 89 92 97	mxidlmaxv	$⊢ φ \to RSpan (R) (M \cup \{X\}) = {Base}_{R}$
99	56 98	eleqtrrd	$⊢ φ \to 1_{R} \in RSpan (R) (M \cup \{X\})$
100	6 7	eldifd	$⊢ φ \to X \in ({Base}_{R} ∖ M)$
101	87 13 61 22 25 60 28 100	elrspunsn	$⊢ φ \to (1_{R} \in RSpan (R) (M \cup \{X\}) \leftrightarrow \exists r \in {Base}_{R} \exists m \in M 1_{R} = (r \cdot_{R} X) +_{R} m)$
102	99 101	mpbid	$⊢ φ \to \exists r \in {Base}_{R} \exists m \in M 1_{R} = (r \cdot_{R} X) +_{R} m$
103	84 102	r19.29vva	$⊢ φ \to \exists v \in {Base}_{Q} v \cdot_{Q} [X] (R ~_{QG} M) = 1_{Q}$

Metamath Proof Explorer

Theorem qsdrngilem

Proof