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

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 ‘ 𝑅 ) )