Metamath Proof Explorer


Theorem mxidlprm

Description: Every maximal ideal is prime. Statement in Lang p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypothesis mxidlprm.1 × = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
Assertion mxidlprm ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mxidlprm.1 × = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
2 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
3 2 adantr ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 mxidlidl ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
6 2 5 sylan ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
7 4 mxidlnr ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ ( Base ‘ 𝑅 ) )
8 2 7 sylan ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ ( Base ‘ 𝑅 ) )
9 simpllr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) )
10 simpr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) )
11 10 oveq2d ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑢 ( +g𝑅 ) 𝑘 ) = ( 𝑢 ( +g𝑅 ) ( 𝑎 ( .r𝑅 ) 𝑥 ) ) )
12 9 11 eqtrd ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) ( 𝑎 ( .r𝑅 ) 𝑥 ) ) )
13 12 oveq1d ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 1r𝑅 ) ( .r𝑅 ) 𝑦 ) = ( ( 𝑢 ( +g𝑅 ) ( 𝑎 ( .r𝑅 ) 𝑥 ) ) ( .r𝑅 ) 𝑦 ) )
14 3 ad4antr ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑅 ∈ Ring )
15 14 ad5antr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑅 ∈ Ring )
16 simp-8r ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
17 eqid ( .r𝑅 ) = ( .r𝑅 )
18 eqid ( 1r𝑅 ) = ( 1r𝑅 )
19 4 17 18 ringlidm ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r𝑅 ) ( .r𝑅 ) 𝑦 ) = 𝑦 )
20 15 16 19 syl2anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 1r𝑅 ) ( .r𝑅 ) 𝑦 ) = 𝑦 )
21 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
22 4 21 lidlss ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
23 6 22 syl ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
24 23 ad4antr ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
25 24 ad5antr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
26 simp-5r ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑢𝑀 )
27 25 26 sseldd ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
28 simplr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
29 simp-4r ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
30 29 ad5antr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
31 4 17 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 ( .r𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
32 15 28 30 31 syl3anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑎 ( .r𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
33 eqid ( +g𝑅 ) = ( +g𝑅 )
34 4 33 17 ringdir ( ( 𝑅 ∈ Ring ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑎 ( .r𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑢 ( +g𝑅 ) ( 𝑎 ( .r𝑅 ) 𝑥 ) ) ( .r𝑅 ) 𝑦 ) = ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ) )
35 15 27 32 16 34 syl13anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 𝑢 ( +g𝑅 ) ( 𝑎 ( .r𝑅 ) 𝑥 ) ) ( .r𝑅 ) 𝑦 ) = ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ) )
36 13 20 35 3eqtr3d ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑦 = ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ) )
37 simp-5r ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
38 14 37 5 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
39 38 ad5antr ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
40 simp-10l ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑅 ∈ CRing )
41 4 17 crngcom ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r𝑅 ) 𝑢 ) = ( 𝑢 ( .r𝑅 ) 𝑦 ) )
42 40 16 27 41 syl3anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑦 ( .r𝑅 ) 𝑢 ) = ( 𝑢 ( .r𝑅 ) 𝑦 ) )
43 21 4 17 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑢𝑀 ) ) → ( 𝑦 ( .r𝑅 ) 𝑢 ) ∈ 𝑀 )
44 15 39 16 26 43 syl22anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑦 ( .r𝑅 ) 𝑢 ) ∈ 𝑀 )
45 42 44 eqeltrrd ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑢 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 )
46 4 17 ringass ( ( 𝑅 ∈ Ring ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) = ( 𝑎 ( .r𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑦 ) ) )
47 15 28 30 16 46 syl13anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) = ( 𝑎 ( .r𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑦 ) ) )
48 simp-7r ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 )
49 21 4 17 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ) → ( 𝑎 ( .r𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑦 ) ) ∈ 𝑀 )
50 15 39 28 48 49 syl22anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( 𝑎 ( .r𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑦 ) ) ∈ 𝑀 )
51 47 50 eqeltrd ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ∈ 𝑀 )
52 21 33 lidlacl ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ∧ ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ) → ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ) ∈ 𝑀 )
53 15 39 45 51 52 syl22anc ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → ( ( 𝑢 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( ( 𝑎 ( .r𝑅 ) 𝑥 ) ( .r𝑅 ) 𝑦 ) ) ∈ 𝑀 )
54 36 53 eqeltrd ( ( ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) → 𝑦𝑀 )
55 simplr ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) → 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) )
56 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
57 56 4 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
58 56 17 mgpplusg ( .r𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
59 fvexd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( mulGrp ‘ 𝑅 ) ∈ V )
60 ssidd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
61 57 58 1 59 60 29 elgrplsmsn ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) )
62 61 ad3antrrr ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) → ( 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) )
63 55 62 mpbid ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) → ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) 𝑘 = ( 𝑎 ( .r𝑅 ) 𝑥 ) )
64 54 63 r19.29a ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑢𝑀 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) → 𝑦𝑀 )
65 4 18 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
66 14 65 syl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
67 eqid ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
68 eqid ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
69 eqid ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
70 69 21 lpiss ( 𝑅 ∈ Ring → ( LPIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
71 14 70 syl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( LPIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
72 4 56 1 68 14 29 lsmsnidl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ∈ ( LPIdeal ‘ 𝑅 ) )
73 71 72 sseldd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ∈ ( LIdeal ‘ 𝑅 ) )
74 4 67 68 14 38 73 lsmidl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∈ ( LIdeal ‘ 𝑅 ) )
75 rlmlmod ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
76 14 75 syl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
77 rlmbas ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
78 rspval ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
79 77 78 lspssid ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ) → 𝑀 ⊆ ( ( RSpan ‘ 𝑅 ) ‘ 𝑀 ) )
80 76 24 79 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ⊆ ( ( RSpan ‘ 𝑅 ) ‘ 𝑀 ) )
81 29 snssd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → { 𝑥 } ⊆ ( Base ‘ 𝑅 ) )
82 4 56 1 14 60 81 ringlsmss ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) )
83 24 82 unssd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ⊆ ( Base ‘ 𝑅 ) )
84 ssun1 𝑀 ⊆ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) )
85 84 a1i ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ⊆ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) )
86 77 78 lspss ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ⊆ ( Base ‘ 𝑅 ) ∧ 𝑀 ⊆ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ 𝑀 ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) )
87 76 83 85 86 syl3anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( RSpan ‘ 𝑅 ) ‘ 𝑀 ) ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) )
88 80 87 sstrd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ⊆ ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) )
89 4 67 68 14 38 73 lsmidllsp ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = ( ( RSpan ‘ 𝑅 ) ‘ ( 𝑀 ∪ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) )
90 88 89 sseqtrrd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑀 ⊆ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) )
91 4 mxidlmax ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑀 ⊆ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ) ) → ( ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = 𝑀 ∨ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = ( Base ‘ 𝑅 ) ) )
92 14 37 74 90 91 syl22anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = 𝑀 ∨ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = ( Base ‘ 𝑅 ) ) )
93 eqid ( 0g𝑅 ) = ( 0g𝑅 )
94 21 93 lidl0cl ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g𝑅 ) ∈ 𝑀 )
95 14 38 94 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 0g𝑅 ) ∈ 𝑀 )
96 oveq1 ( 𝑎 = ( 0g𝑅 ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) )
97 96 eqeq2d ( 𝑎 = ( 0g𝑅 ) → ( 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ↔ 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) ) )
98 97 rexbidv ( 𝑎 = ( 0g𝑅 ) → ( ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ↔ ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) ) )
99 98 adantl ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑎 = ( 0g𝑅 ) ) → ( ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ↔ ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) ) )
100 oveq1 ( 𝑎 = ( 1r𝑅 ) → ( 𝑎 ( .r𝑅 ) 𝑥 ) = ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) )
101 100 eqeq2d ( 𝑎 = ( 1r𝑅 ) → ( 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ↔ 𝑥 = ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) ) )
102 101 adantl ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑎 = ( 1r𝑅 ) ) → ( 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ↔ 𝑥 = ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) ) )
103 4 17 18 ringlidm ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) = 𝑥 )
104 14 29 103 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) = 𝑥 )
105 104 eqcomd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑥 = ( ( 1r𝑅 ) ( .r𝑅 ) 𝑥 ) )
106 66 102 105 rspcedvd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑥 ) )
107 57 58 1 59 60 29 elgrplsmsn ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑥 ) ) )
108 106 107 mpbird ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) )
109 oveq2 ( 𝑏 = 𝑥 → ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) )
110 109 eqeq2d ( 𝑏 = 𝑥 → ( 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) ↔ 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) ) )
111 110 adantl ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) ∧ 𝑏 = 𝑥 ) → ( 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) ↔ 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) ) )
112 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
113 14 112 syl ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑅 ∈ Grp )
114 4 33 93 grplid ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) = 𝑥 )
115 113 29 114 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) = 𝑥 )
116 115 eqcomd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑥 ) )
117 108 111 116 rspcedvd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ∃ 𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( ( 0g𝑅 ) ( +g𝑅 ) 𝑏 ) )
118 95 99 117 rspcedvd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ∃ 𝑎𝑀𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) )
119 simp-5l ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑅 ∈ CRing )
120 4 33 67 lsmelvalx ( ( 𝑅 ∈ CRing ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ∧ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ↔ ∃ 𝑎𝑀𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
121 119 24 82 120 syl3anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑥 ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ↔ ∃ 𝑎𝑀𝑏 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
122 118 121 mpbird ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑥 ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) )
123 simpr ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ¬ 𝑥𝑀 )
124 nelne1 ( ( 𝑥 ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ≠ 𝑀 )
125 122 123 124 syl2anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ≠ 𝑀 )
126 125 neneqd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ¬ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = 𝑀 )
127 92 126 orcnd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) = ( Base ‘ 𝑅 ) )
128 66 127 eleqtrrd ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( 1r𝑅 ) ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) )
129 4 33 67 lsmelvalx ( ( 𝑅 ∈ CRing ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ∧ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( 1r𝑅 ) ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ↔ ∃ 𝑢𝑀𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) )
130 119 24 82 129 syl3anc ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ( ( 1r𝑅 ) ∈ ( 𝑀 ( LSSum ‘ 𝑅 ) ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ) ↔ ∃ 𝑢𝑀𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) ) )
131 128 130 mpbid ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → ∃ 𝑢𝑀𝑘 ∈ ( ( Base ‘ 𝑅 ) × { 𝑥 } ) ( 1r𝑅 ) = ( 𝑢 ( +g𝑅 ) 𝑘 ) )
132 64 131 r19.29vva ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) ∧ ¬ 𝑥𝑀 ) → 𝑦𝑀 )
133 132 ex ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) → ( ¬ 𝑥𝑀𝑦𝑀 ) )
134 133 orrd ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 ) → ( 𝑥𝑀𝑦𝑀 ) )
135 134 ex ( ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 → ( 𝑥𝑀𝑦𝑀 ) ) )
136 135 anasss ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 → ( 𝑥𝑀𝑦𝑀 ) ) )
137 136 ralrimivva ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 → ( 𝑥𝑀𝑦𝑀 ) ) )
138 4 17 prmidl2 ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑀 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑀 → ( 𝑥𝑀𝑦𝑀 ) ) ) ) → 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) )
139 3 6 8 137 138 syl22anc ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( PrmIdeal ‘ 𝑅 ) )