Metamath Proof Explorer

Theorem qsdrnglem2

Description: Lemma for qsdrng . (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses qsdrng.0 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
qsdrng.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
qsdrng.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
qsdrng.2 ⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
qsdrnglem2.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
qsdrnglem2.q ⊢ ( 𝜑 → 𝑄 ∈ DivRing )
qsdrnglem2.j ⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
qsdrnglem2.m ⊢ ( 𝜑 → 𝑀 ⊆ 𝐽 )
qsdrnglem2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐽 ∖ 𝑀 ) )
Assertion qsdrnglem2 ( 𝜑 → 𝐽 = 𝐵 )

Proof

Step Hyp Ref Expression
1 qsdrng.0 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 qsdrng.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
3 qsdrng.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4 qsdrng.2 ⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
5 qsdrnglem2.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 qsdrnglem2.q ⊢ ( 𝜑 → 𝑄 ∈ DivRing )
7 qsdrnglem2.j ⊢ ( 𝜑 → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
8 qsdrnglem2.m ⊢ ( 𝜑 → 𝑀 ⊆ 𝐽 )
9 qsdrnglem2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐽 ∖ 𝑀 ) )
10 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
11 3 10 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑅 ∈ Ring )
13 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝐽 ∈ ( LIdeal ‘ 𝑅 ) )
14 12 ringgrpd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑅 ∈ Grp )
15 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
16 5 15 lidlss ⊢ ( 𝐽 ∈ ( LIdeal ‘ 𝑅 ) → 𝐽 ⊆ 𝐵 )
17 13 16 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝐽 ⊆ 𝐵 )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑠 ∈ 𝐵 )
19 9 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑋 ∈ 𝐽 )
21 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
22 15 5 21 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑋 ∈ 𝐽 ) ) → ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐽 )
23 12 13 18 20 22 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐽 )
24 17 23 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 5 25 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
27 12 26 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
28 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
29 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
30 5 28 29 grpasscan1 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
31 14 24 27 30 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 1r ‘ 𝑅 ) )
32 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ⊆ 𝐽 )
33 7 16 syl ⊢ ( 𝜑 → 𝐽 ⊆ 𝐵 )
34 8 33 sstrd ⊢ ( 𝜑 → 𝑀 ⊆ 𝐵 )
35 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ⊆ 𝐵 )
36 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
37 36 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) )
38 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
39 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
40 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
41 eqid ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
42 eqid ⊢ ( invr ‘ 𝑄 ) = ( invr ‘ 𝑄 )
43 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑄 ∈ DivRing )
44 33 19 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
45 ovex ⊢ ( 𝑅 ~QG 𝑀 ) ∈ V
46 45 ecelqsi ⊢ ( 𝑋 ∈ 𝐵 → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ∈ ( 𝐵 / ( 𝑅 ~QG 𝑀 ) ) )
47 44 46 syl ⊢ ( 𝜑 → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ∈ ( 𝐵 / ( 𝑅 ~QG 𝑀 ) ) )
48 2 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) )
49 5 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
50 45 a1i ⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) ∈ V )
51 48 49 50 3 qusbas ⊢ ( 𝜑 → ( 𝐵 / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) )
52 47 51 eleqtrd ⊢ ( 𝜑 → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
54 4 2idllidld ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
55 15 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
56 11 54 55 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
57 eqid ⊢ ( 𝑅 ~QG 𝑀 ) = ( 𝑅 ~QG 𝑀 )
58 5 57 eqger ⊢ ( 𝑀 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝑀 ) Er 𝐵 )
59 56 58 syl ⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) Er 𝐵 )
60 ecref ⊢ ( ( ( 𝑅 ~QG 𝑀 ) Er 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) )
61 59 44 60 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) )
62 9 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑀 )
63 nelne1 ⊢ ( ( 𝑋 ∈ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ∧ ¬ 𝑋 ∈ 𝑀 ) → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ≠ 𝑀 )
64 61 62 63 syl2anc ⊢ ( 𝜑 → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ≠ 𝑀 )
65 lidlnsg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) )
66 11 54 65 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) )
67 2 qus0g ⊢ ( 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) → ( 0g ‘ 𝑄 ) = 𝑀 )
68 66 67 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑄 ) = 𝑀 )
69 64 68 neeqtrrd ⊢ ( 𝜑 → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ≠ ( 0g ‘ 𝑄 ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ≠ ( 0g ‘ 𝑄 ) )
71 38 39 40 41 42 43 53 70 drnginvrld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) )
72 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
73 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑋 ∈ 𝐵 )
74 2 5 21 40 12 72 18 73 qusmul2idl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) )
75 37 71 74 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) )
76 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
77 2 76 25 qus1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( 𝑄 ∈ Ring ∧ [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) ) )
78 77 simprd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) → [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) )
79 12 72 78 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 1r ‘ 𝑄 ) )
80 75 79 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) = [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) )
81 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
82 81 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑅 ~QG 𝑀 ) Er 𝐵 )
83 82 27 erth2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ↔ [ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ] ( 𝑅 ~QG 𝑀 ) = [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) ) )
84 80 83 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) )
85 5 29 28 57 eqgval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ 𝐵 ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ↔ ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 ) ) )
86 85 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ 𝐵 ) ∧ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 ) )
87 86 simp3d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ 𝐵 ) ∧ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( 𝑅 ~QG 𝑀 ) ( 1r ‘ 𝑅 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 )
88 12 35 84 87 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝑀 )
89 32 88 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝐽 )
90 15 28 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝐽 ∧ ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ 𝐽 ) ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ∈ 𝐽 )
91 12 13 23 89 90 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑠 ( .r ‘ 𝑅 ) 𝑋 ) ) ( +g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ∈ 𝐽 )
92 31 91 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐽 )
93 15 5 25 lidl1el ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝐽 ↔ 𝐽 = 𝐵 ) )
94 93 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐽 ) → 𝐽 = 𝐵 )
95 12 13 92 94 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝐽 = 𝐵 )
96 38 39 42 6 52 69 drnginvrcld ⊢ ( 𝜑 → ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ∈ ( Base ‘ 𝑄 ) )
97 96 51 eleqtrrd ⊢ ( 𝜑 → ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ∈ ( 𝐵 / ( 𝑅 ~QG 𝑀 ) ) )
98 elqsi ⊢ ( ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) ∈ ( 𝐵 / ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑠 ∈ 𝐵 ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
99 97 98 syl ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐵 ( ( invr ‘ 𝑄 ) ‘ [ 𝑋 ] ( 𝑅 ~QG 𝑀 ) ) = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
100 95 99 r19.29a ⊢ ( 𝜑 → 𝐽 = 𝐵 )