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

Metamath Proof Explorer

Theorem qsidomlem2

Description: A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 qsidom.1 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
2 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
3 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
4 2 3 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6 1 5 quscrng ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑄 ∈ CRing )
7 4 6 syldan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ CRing )
8 5 crng2idl ⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
9 8 eleq2d ⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) )
10 9 biimpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
11 4 10 syldan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
12 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
13 1 12 qusring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
14 2 11 13 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
15 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
16 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
17 15 16 ring0cl ⊢ ( 𝑄 ∈ Ring → ( 0g ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
18 14 17 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
19 18 snssd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { ( 0g ‘ 𝑄 ) } ⊆ ( Base ‘ 𝑄 ) )
20 lidlnsg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
21 2 20 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
22 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
23 1 22 qus0 ⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
24 21 23 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = ( 0g ‘ 𝑄 ) )
25 5 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
26 2 25 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
27 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
28 eqid ⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
29 27 28 22 eqgid ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
30 26 29 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
31 24 30 eqtr3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑄 ) = 𝐼 )
32 4 31 syldan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑄 ) = 𝐼 )
33 32 sneqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { ( 0g ‘ 𝑄 ) } = { 𝐼 } )
34 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
35 27 34 isprmidlc ⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ) ) )
36 35 biimpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ) )
37 36 simp2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ≠ ( Base ‘ 𝑅 ) )
38 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
39 2 38 syl ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
40 39 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝑅 ∈ Grp )
41 2 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝑅 ∈ Ring )
42 4 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
43 41 42 25 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
44 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → ( Base ‘ 𝑄 ) = { 𝐼 } )
45 27 1 qustrivr ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝐼 = ( Base ‘ 𝑅 ) )
46 40 43 44 45 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑄 ) = { 𝐼 } ) → 𝐼 = ( Base ‘ 𝑅 ) )
47 37 46 mteqand ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( Base ‘ 𝑄 ) ≠ { 𝐼 } )
48 47 necomd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { 𝐼 } ≠ ( Base ‘ 𝑄 ) )
49 33 48 eqnetrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → { ( 0g ‘ 𝑄 ) } ≠ ( Base ‘ 𝑄 ) )
50 pssdifn0 ⊢ ( ( { ( 0g ‘ 𝑄 ) } ⊆ ( Base ‘ 𝑄 ) ∧ { ( 0g ‘ 𝑄 ) } ≠ ( Base ‘ 𝑄 ) ) → ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ≠ ∅ )
51 19 49 50 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ≠ ∅ )
52 n0 ⊢ ( ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) )
53 51 52 sylib ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∃ 𝑥 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) )
54 16 15 ringelnzr ⊢ ( ( 𝑄 ∈ Ring ∧ 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → 𝑄 ∈ NzRing )
55 54 ex ⊢ ( 𝑄 ∈ Ring → ( 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) → 𝑄 ∈ NzRing ) )
56 55 exlimdv ⊢ ( 𝑄 ∈ Ring → ( ∃ 𝑥 𝑥 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) → 𝑄 ∈ NzRing ) )
57 14 53 56 sylc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ NzRing )
58 36 simp3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
59 58 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
60 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
61 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
62 simp-8l ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑅 ∈ CRing )
63 62 39 syl ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑅 ∈ Grp )
64 4 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
65 62 64 26 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
66 1 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
67 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
68 27 28 eqger ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ~QG 𝐼 ) Er ( Base ‘ 𝑅 ) )
69 26 68 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝐼 ) Er ( Base ‘ 𝑅 ) )
70 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
71 27 28 12 34 2idlcpbl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( 𝑔 ( 𝑅 ~QG 𝐼 ) 𝑒 ∧ ℎ ( 𝑅 ~QG 𝐼 ) 𝑓 ) → ( 𝑔 ( .r ‘ 𝑅 ) ℎ ) ( 𝑅 ~QG 𝐼 ) ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ) )
72 2 10 71 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑔 ( 𝑅 ~QG 𝐼 ) 𝑒 ∧ ℎ ( 𝑅 ~QG 𝐼 ) 𝑓 ) → ( 𝑔 ( .r ‘ 𝑅 ) ℎ ) ( 𝑅 ~QG 𝐼 ) ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ) )
73 2 ad2antrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
74 simprl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑒 ∈ ( Base ‘ 𝑅 ) )
75 simprr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑓 ∈ ( Base ‘ 𝑅 ) )
76 27 34 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Base ‘ 𝑅 ) )
77 73 74 75 76 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒 ∈ ( Base ‘ 𝑅 ) ∧ 𝑓 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Base ‘ 𝑅 ) )
78 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
79 66 67 69 70 72 77 34 78 qusmulval ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) )
80 62 64 60 61 79 syl211anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) )
81 simpr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) )
82 81 ad4antr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) )
83 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) )
84 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) )
85 83 84 oveq12d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) )
86 62 64 31 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 0g ‘ 𝑄 ) = 𝐼 )
87 82 85 86 3eqtr3d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) = 𝐼 )
88 80 87 eqtr3d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 )
89 28 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
90 89 biimpa ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ [ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
91 63 65 88 90 syl21anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
92 rsp2 ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ) )
93 92 impl ⊢ ( ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) )
94 93 imp ⊢ ( ( ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) )
95 59 60 61 91 94 syl1111anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) )
96 86 eqeq2d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ↔ 𝑎 = 𝐼 ) )
97 83 eqeq1d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 = 𝐼 ↔ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ) )
98 28 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑥 ∈ 𝐼 ) )
99 63 65 98 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑥 ∈ 𝐼 ) )
100 96 97 99 3bitrrd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↔ 𝑎 = ( 0g ‘ 𝑄 ) ) )
101 86 eqeq2d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑏 = ( 0g ‘ 𝑄 ) ↔ 𝑏 = 𝐼 ) )
102 84 eqeq1d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑏 = 𝐼 ↔ [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ) )
103 28 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
104 63 65 103 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) = 𝐼 ↔ 𝑦 ∈ 𝐼 ) )
105 101 102 104 3bitrrd ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑦 ∈ 𝐼 ↔ 𝑏 = ( 0g ‘ 𝑄 ) ) )
106 100 105 orbi12d ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( ( 𝑥 ∈ 𝐼 ∨ 𝑦 ∈ 𝐼 ) ↔ ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) ) )
107 95 106 mpbid ⊢ ( ( ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) )
108 simplr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → 𝑏 ∈ ( Base ‘ 𝑄 ) )
109 1 a1i ⊢ ( 𝑅 ∈ CRing → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) )
110 eqidd ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
111 ovexd ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ~QG 𝐼 ) ∈ V )
112 id ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ CRing )
113 109 110 111 112 qusbas ⊢ ( 𝑅 ∈ CRing → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
114 113 ad4antr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) = ( Base ‘ 𝑄 ) )
115 108 114 eleqtrrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
116 115 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
117 elqsi ⊢ ( 𝑏 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) )
118 116 117 syl ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) 𝑏 = [ 𝑦 ] ( 𝑅 ~QG 𝐼 ) )
119 107 118 r19.29a ⊢ ( ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) )
120 simpllr ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → 𝑎 ∈ ( Base ‘ 𝑄 ) )
121 120 114 eleqtrrd ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → 𝑎 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) )
122 elqsi ⊢ ( 𝑎 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝐼 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) )
123 121 122 syl ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑎 = [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) )
124 119 123 r19.29a ⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) )
125 124 ex ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) → ( ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) ) )
126 125 anasss ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑄 ) ∧ 𝑏 ∈ ( Base ‘ 𝑄 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) ) )
127 126 ralrimivva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑎 ∈ ( Base ‘ 𝑄 ) ∀ 𝑏 ∈ ( Base ‘ 𝑄 ) ( ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) ) )
128 15 78 16 isdomn ⊢ ( 𝑄 ∈ Domn ↔ ( 𝑄 ∈ NzRing ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑄 ) ∀ 𝑏 ∈ ( Base ‘ 𝑄 ) ( ( 𝑎 ( .r ‘ 𝑄 ) 𝑏 ) = ( 0g ‘ 𝑄 ) → ( 𝑎 = ( 0g ‘ 𝑄 ) ∨ 𝑏 = ( 0g ‘ 𝑄 ) ) ) ) )
129 57 127 128 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ Domn )
130 isidom ⊢ ( 𝑄 ∈ IDomn ↔ ( 𝑄 ∈ CRing ∧ 𝑄 ∈ Domn ) )
131 7 129 130 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ IDomn )