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

Metamath Proof Explorer

Theorem qsidomlem1

Description: If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024)

Ref Expression
Hypothesis qsidom.1 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
Assertion qsidomlem1 ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 qsidom.1 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
2 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
3 2 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝑅 ∈ Ring )
4 simplr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 𝐼 = ( Base ‘ 𝑅 ) )
6 5 oveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) )
7 6 oveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) = ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) )
8 1 7 eqtrid ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) )
9 8 fveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( Base ‘ 𝑄 ) = ( Base ‘ ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) ) )
10 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
11 2 10 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
12 11 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) = ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) )
15 13 14 qustriv ⊢ ( 𝑅 ∈ Grp → ( Base ‘ ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) ) = { ( Base ‘ 𝑅 ) } )
16 12 15 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( Base ‘ ( 𝑅 /s ( 𝑅 ~QG ( Base ‘ 𝑅 ) ) ) ) = { ( Base ‘ 𝑅 ) } )
17 9 16 eqtrd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( Base ‘ 𝑄 ) = { ( Base ‘ 𝑅 ) } )
18 17 fveq2d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ ( Base ‘ 𝑄 ) ) = ( ♯ ‘ { ( Base ‘ 𝑅 ) } ) )
19 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
20 hashsng ⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ♯ ‘ { ( Base ‘ 𝑅 ) } ) = 1 )
21 19 20 ax-mp ⊢ ( ♯ ‘ { ( Base ‘ 𝑅 ) } ) = 1
22 18 21 eqtrdi ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ ( Base ‘ 𝑄 ) ) = 1 )
23 1red ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 1 ∈ ℝ )
24 isidom ⊢ ( 𝑄 ∈ IDomn ↔ ( 𝑄 ∈ CRing ∧ 𝑄 ∈ Domn ) )
25 24 simprbi ⊢ ( 𝑄 ∈ IDomn → 𝑄 ∈ Domn )
26 domnnzr ⊢ ( 𝑄 ∈ Domn → 𝑄 ∈ NzRing )
27 25 26 syl ⊢ ( 𝑄 ∈ IDomn → 𝑄 ∈ NzRing )
28 27 ad2antlr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 𝑄 ∈ NzRing )
29 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
30 29 isnzr2hash ⊢ ( 𝑄 ∈ NzRing ↔ ( 𝑄 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑄 ) ) ) )
31 30 simprbi ⊢ ( 𝑄 ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ 𝑄 ) ) )
32 28 31 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → 1 < ( ♯ ‘ ( Base ‘ 𝑄 ) ) )
33 23 32 gtned ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ ( Base ‘ 𝑄 ) ) ≠ 1 )
34 33 neneqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝐼 = ( Base ‘ 𝑅 ) ) → ¬ ( ♯ ‘ ( Base ‘ 𝑄 ) ) = 1 )
35 22 34 pm2.65da ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → ¬ 𝐼 = ( Base ‘ 𝑅 ) )
36 35 neqned ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝐼 ≠ ( Base ‘ 𝑅 ) )
37 25 ad4antlr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → 𝑄 ∈ Domn )
38 ovex ⊢ ( 𝑅 ~QG 𝐼 ) ∈ V
39 38 ecelqsi ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
40 39 ad3antlr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
41 simp-5l ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → 𝑅 ∈ CRing )
42 1 a1i ⊢ ( 𝑅 ∈ CRing → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
43 eqidd ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
44 ovexd ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ~QG 𝐼 ) ∈ V )
45 id ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
46 42 43 44 45 qusbas ⊢ ( 𝑅 ∈ CRing → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
47 41 46 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
48 40 47 eleqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) )
49 38 ecelqsi ⊢ ( 𝑦 ∈ ( Base ‘ 𝑅 ) → [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
50 49 ad2antlr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
51 50 47 eleqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) )
52 41 2 10 3syl ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → 𝑅 ∈ Grp )
53 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
54 53 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
55 2 54 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
56 55 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
57 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
58 eqid ⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
59 58 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
60 59 biimpar ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
61 52 56 57 60 syl21anc ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
62 1 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
63 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
64 13 58 eqger ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝐼 ) Er ( Base ‘ 𝑅 ) )
65 55 64 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝐼 ) Er ( Base ‘ 𝑅 ) )
66 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
67 53 crng2idl ⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
68 67 eleq2d ⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) )
69 68 biimpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
70 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
71 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
72 13 58 70 71 2idlcpbl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( 𝑔 ( 𝑅 ~QG 𝐼 ) 𝑒 ∧ ℎ ( 𝑅 ~QG 𝐼 ) 𝑓 ) → ( 𝑔 ( .r ‘ 𝑅 ) ℎ ) ( 𝑅 ~QG 𝐼 ) ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ) )
73 2 69 72 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑔 ( 𝑅 ~QG 𝐼 ) 𝑒 ∧ ℎ ( 𝑅 ~QG 𝐼 ) 𝑓 ) → ( 𝑔 ( .r ‘ 𝑅 ) ℎ ) ( 𝑅 ~QG 𝐼 ) ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ) )
74 2 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
75 simprl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑒 ∈ ( Base ‘ 𝑅 ) )
76 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑓 ∈ ( Base ‘ 𝑅 ) )
77 13 71 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Base ‘ 𝑅 ) )
78 74 75 76 77 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Base ‘ 𝑅 ) )
79 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
80 62 63 65 66 73 78 71 79 qusmulval ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) )
81 80 ad5ant134 ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) )
82 lidlnsg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
83 2 82 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
84 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
85 1 84 qus0 ⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
86 83 85 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
87 13 58 84 eqgid ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
88 55 87 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
89 86 88 eqtr3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑄 ) = 𝐼 )
90 89 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( 0g ‘ 𝑄 ) = 𝐼 )
91 61 81 90 3eqtr4d ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = ( 0g ‘ 𝑄 ) )
92 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
93 29 79 92 domneq0 ⊢ ( ( 𝑄 ∈ Domn ∧ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) ∧ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = ( 0g ‘ 𝑄 ) ↔ ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ∨ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ) ) )
94 93 biimpa ⊢ ( ( ( 𝑄 ∈ Domn ∧ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) ∧ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ∈ ( Base ‘ 𝑄 ) ) ∧ ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = ( 0g ‘ 𝑄 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ∨ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ) )
95 37 48 51 91 94 syl31anc ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ∨ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ) )
96 89 eqeq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ↔ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ) )
97 66 2 10 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
98 58 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑥 ∈ 𝐼 ) )
99 97 55 98 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑥 ∈ 𝐼 ) )
100 96 99 bitrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ↔ 𝑥 ∈ 𝐼 ) )
101 89 eqeq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ↔ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ) )
102 58 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
103 97 55 102 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
104 101 103 bitrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ↔ 𝑦 ∈ 𝐼 ) )
105 100 104 orbi12d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ∨ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ) ↔ ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
106 105 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ∨ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) ) ↔ ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
107 95 106 mpbid ⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) )
108 107 ex ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
109 108 anasss ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
110 109 ralrimivva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
111 13 71 prmidl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝐼 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ) ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )
112 3 4 36 110 111 syl22anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )