Metamath Proof Explorer


Theorem qsdrngilem

Description: Lemma for qsdrngi . (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses qsdrng.0 𝑂 = ( oppr𝑅 )
qsdrng.q 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
qsdrng.r ( 𝜑𝑅 ∈ NzRing )
qsdrngi.1 ( 𝜑𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
qsdrngi.2 ( 𝜑𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) )
qsdrngilem.1 ( 𝜑𝑋 ∈ ( Base ‘ 𝑅 ) )
qsdrngilem.2 ( 𝜑 → ¬ 𝑋𝑀 )
Assertion qsdrngilem ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( 𝑣 ( .r𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r𝑄 ) )

Proof

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𝑄 ) )