This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 qusmul2idl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( 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 ‘ 𝑄 ) )