Step |
Hyp |
Ref |
Expression |
1 |
|
qsdrng.0 |
⊢ 𝑂 = ( oppr ‘ 𝑅 ) |
2 |
|
qsdrng.q |
⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) |
3 |
|
qsdrng.r |
⊢ ( 𝜑 → 𝑅 ∈ NzRing ) |
4 |
|
qsdrngi.1 |
⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) |
5 |
|
qsdrngi.2 |
⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) ) |
6 |
|
qsdrngilem.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) ) |
7 |
|
qsdrngilem.2 |
⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑀 ) |
8 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) ) |
9 |
|
ovex |
⊢ ( 𝑅 ~QG 𝑀 ) ∈ V |
10 |
9
|
ecelqsi |
⊢ ( 𝑟 ∈ ( Base ‘ 𝑅 ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) ) |
11 |
8 10
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) ) |
12 |
2
|
a1i |
⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) ) |
13 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
14 |
13
|
a1i |
⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) |
15 |
|
ovexd |
⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) ∈ V ) |
16 |
12 14 15 3
|
qusbas |
⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) ) |
17 |
16
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) ) |
18 |
11 17
|
eleqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( Base ‘ 𝑄 ) ) |
19 |
|
oveq1 |
⊢ ( 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) → ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ) |
20 |
19
|
eqeq1d |
⊢ ( 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) → ( ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ↔ ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ) |
21 |
20
|
adantl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ↔ ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ) |
22 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
23 |
|
eqid |
⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 ) |
24 |
|
nzrring |
⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring ) |
25 |
3 24
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
26 |
25
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑅 ∈ Ring ) |
27 |
13
|
mxidlidl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) |
28 |
25 4 27
|
syl2anc |
⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) |
29 |
1
|
opprring |
⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring ) |
30 |
25 29
|
syl |
⊢ ( 𝜑 → 𝑂 ∈ Ring ) |
31 |
|
eqid |
⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) |
32 |
31
|
mxidlidl |
⊢ ( ( 𝑂 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑂 ) ) |
33 |
30 5 32
|
syl2anc |
⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑂 ) ) |
34 |
28 33
|
elind |
⊢ ( 𝜑 → 𝑀 ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) ) |
35 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
36 |
|
eqid |
⊢ ( LIdeal ‘ 𝑂 ) = ( LIdeal ‘ 𝑂 ) |
37 |
|
eqid |
⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) |
38 |
35 1 36 37
|
2idlval |
⊢ ( 2Ideal ‘ 𝑅 ) = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) |
39 |
34 38
|
eleqtrrdi |
⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) |
40 |
39
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) |
41 |
6
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) ) |
42 |
2 13 22 23 26 40 8 41
|
qusmul2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) ) |
43 |
|
lidlnsg |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) ) |
44 |
25 28 43
|
syl2anc |
⊢ ( 𝜑 → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) ) |
45 |
|
nsgsubg |
⊢ ( 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) ) |
46 |
|
eqid |
⊢ ( 𝑅 ~QG 𝑀 ) = ( 𝑅 ~QG 𝑀 ) |
47 |
13 46
|
eqger |
⊢ ( 𝑀 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑀 ) Er ( Base ‘ 𝑅 ) ) |
48 |
44 45 47
|
3syl |
⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) Er ( Base ‘ 𝑅 ) ) |
49 |
48
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑅 ~QG 𝑀 ) Er ( Base ‘ 𝑅 ) ) |
50 |
13 35
|
lidlss |
⊢ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) ) |
51 |
28 50
|
syl |
⊢ ( 𝜑 → 𝑀 ⊆ ( Base ‘ 𝑅 ) ) |
52 |
51
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) ) |
53 |
13 22 26 8 41
|
ringcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) |
54 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
55 |
13 54
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
56 |
25 55
|
syl |
⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
57 |
56
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) |
58 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) |
59 |
58
|
oveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) ) |
60 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
61 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
62 |
|
eqid |
⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 ) |
63 |
25
|
ringgrpd |
⊢ ( 𝜑 → 𝑅 ∈ Grp ) |
64 |
63
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑅 ∈ Grp ) |
65 |
13 60 61 62 64 53
|
grplinvd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) |
66 |
65
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑚 ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑚 ) ) |
67 |
13 62 64 53
|
grpinvcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∈ ( Base ‘ 𝑅 ) ) |
68 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑚 ∈ 𝑀 ) |
69 |
52 68
|
sseldd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑚 ∈ ( Base ‘ 𝑅 ) ) |
70 |
13 60 64 67 53 69
|
grpassd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) 𝑚 ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) ) |
71 |
13 60 61 64 69
|
grplidd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑚 ) = 𝑚 ) |
72 |
66 70 71
|
3eqtr3d |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) = 𝑚 ) |
73 |
59 72
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑚 ) |
74 |
73 68
|
eqeltrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 ) |
75 |
13 62 60 46
|
eqgval |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ↔ ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 ) ) ) |
76 |
75
|
biimpar |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ) |
77 |
26 52 53 57 74 76
|
syl23anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ) |
78 |
49 77
|
erthi |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → [ ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) = [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) ) |
79 |
42 78
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) ) |
80 |
2 37 54
|
qus1 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( 𝑄 ∈ Ring ∧ [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) ) ) |
81 |
80
|
simprd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) → [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) ) |
82 |
26 40 81
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) ) |
83 |
79 82
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) |
84 |
18 21 83
|
rspcedvd |
⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑀 ) ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) |
85 |
6
|
snssd |
⊢ ( 𝜑 → { 𝑋 } ⊆ ( Base ‘ 𝑅 ) ) |
86 |
51 85
|
unssd |
⊢ ( 𝜑 → ( 𝑀 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑅 ) ) |
87 |
|
eqid |
⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 ) |
88 |
87 13 35
|
rspcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ) |
89 |
25 86 88
|
syl2anc |
⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ) |
90 |
87 13
|
rspssid |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ∪ { 𝑋 } ) ⊆ ( Base ‘ 𝑅 ) ) → ( 𝑀 ∪ { 𝑋 } ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
91 |
25 86 90
|
syl2anc |
⊢ ( 𝜑 → ( 𝑀 ∪ { 𝑋 } ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
92 |
91
|
unssad |
⊢ ( 𝜑 → 𝑀 ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
93 |
91
|
unssbd |
⊢ ( 𝜑 → { 𝑋 } ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
94 |
|
snssg |
⊢ ( 𝑋 ∈ ( Base ‘ 𝑅 ) → ( 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ↔ { 𝑋 } ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) ) |
95 |
94
|
biimpar |
⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ { 𝑋 } ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
96 |
6 93 95
|
syl2anc |
⊢ ( 𝜑 → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
97 |
96 7
|
eldifd |
⊢ ( 𝜑 → 𝑋 ∈ ( ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ∖ 𝑀 ) ) |
98 |
13 25 4 89 92 97
|
mxidlmaxv |
⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) = ( Base ‘ 𝑅 ) ) |
99 |
56 98
|
eleqtrrd |
⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ) |
100 |
6 7
|
eldifd |
⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑀 ) ) |
101 |
87 13 61 22 25 60 28 100
|
elrspunsn |
⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ { 𝑋 } ) ) ↔ ∃ 𝑟 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ 𝑀 ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) ) |
102 |
99 101
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝑅 ) ∃ 𝑚 ∈ 𝑀 ( 1r ‘ 𝑅 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) 𝑚 ) ) |
103 |
84 102
|
r19.29vva |
⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) |