Metamath Proof Explorer

Theorem qsdrngi

Description: A quotient by a maximal left and maximal right ideal is a division ring. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses qsdrng.0 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
qsdrng.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
qsdrng.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
qsdrngi.1 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
qsdrngi.2 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) )
Assertion qsdrngi ( 𝜑 → 𝑄 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 qsdrng.0 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 qsdrng.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
3 qsdrng.r ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4 qsdrngi.1 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
5 qsdrngi.2 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
8 3 7 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 6 mxidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
10 8 4 9 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
11 1 opprring ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
12 8 11 syl ⊢ ( 𝜑 → 𝑂 ∈ Ring )
13 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
14 13 mxidlidl ⊢ ( ( 𝑂 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑂 ) )
15 12 5 14 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑂 ) )
16 10 15 elind ⊢ ( 𝜑 → 𝑀 ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) ) )
17 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
18 eqid ⊢ ( LIdeal ‘ 𝑂 ) = ( LIdeal ‘ 𝑂 )
19 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
20 17 1 18 19 2idlval ⊢ ( 2Ideal ‘ 𝑅 ) = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ 𝑂 ) )
21 16 20 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
22 6 mxidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ ( Base ‘ 𝑅 ) )
23 8 4 22 syl2anc ⊢ ( 𝜑 → 𝑀 ≠ ( Base ‘ 𝑅 ) )
24 2 6 8 3 21 23 qsnzr ⊢ ( 𝜑 → 𝑄 ∈ NzRing )
25 eqid ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
26 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
27 25 26 nzrnz ⊢ ( 𝑄 ∈ NzRing → ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) )
28 24 27 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) )
29 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
30 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
31 eqid ⊢ ( Unit ‘ 𝑄 ) = ( Unit ‘ 𝑄 )
32 2 19 qusring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
33 8 21 32 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ Ring )
34 33 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
35 34 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑄 ∈ Ring )
36 eldifi ⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) → 𝑢 ∈ ( Base ‘ 𝑄 ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → 𝑢 ∈ ( Base ‘ 𝑄 ) )
38 37 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑢 ∈ ( Base ‘ 𝑄 ) )
39 ovex ⊢ ( 𝑅 ~QG 𝑀 ) ∈ V
40 39 ecelqsi ⊢ ( 𝑟 ∈ ( Base ‘ 𝑅 ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
41 40 ad4antlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
42 2 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) ) )
43 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
44 ovexd ⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) ∈ V )
45 42 43 44 3 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) )
47 46 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) )
48 41 47 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
49 39 ecelqsi ⊢ ( 𝑠 ∈ ( Base ‘ 𝑅 ) → [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
50 49 ad2antlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
51 50 47 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ∈ ( Base ‘ 𝑄 ) )
52 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) )
53 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) )
54 53 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = 𝑢 )
55 52 54 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) 𝑢 ) )
56 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) )
57 55 56 eqtr3d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) )
58 eqid ⊢ ( oppr ‘ 𝑄 ) = ( oppr ‘ 𝑄 )
59 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑄 ) ) = ( .r ‘ ( oppr ‘ 𝑄 ) )
60 29 30 58 59 opprmul ⊢ ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑢 ) = ( 𝑢 ( .r ‘ 𝑄 ) [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
61 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
62 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑅 ∈ Ring )
63 62 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑅 ∈ Ring )
64 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
65 64 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
66 6 1 2 63 65 29 51 38 opprqusmulr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑢 ) = ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) 𝑢 ) )
67 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
68 6 17 lidlss ⊢ ( 𝑀 ∈ ( LIdeal ‘ 𝑅 ) → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
69 10 68 syl ⊢ ( 𝜑 → 𝑀 ⊆ ( Base ‘ 𝑅 ) )
70 1 6 oppreqg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝑀 ) = ( 𝑂 ~QG 𝑀 ) )
71 8 69 70 syl2anc ⊢ ( 𝜑 → ( 𝑅 ~QG 𝑀 ) = ( 𝑂 ~QG 𝑀 ) )
72 71 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 ~QG 𝑀 ) = ( 𝑂 ~QG 𝑀 ) )
73 72 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑅 ~QG 𝑀 ) = ( 𝑂 ~QG 𝑀 ) )
74 73 eceq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) )
75 53 74 eqtr2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) = 𝑢 )
76 67 75 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) 𝑢 ) )
77 66 76 eqtr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑢 ) = ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) )
78 58 25 oppr1 ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ ( oppr ‘ 𝑄 ) )
79 6 1 2 8 21 opprqus1r ⊢ ( 𝜑 → ( 1r ‘ ( oppr ‘ 𝑄 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
80 78 79 eqtrid ⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
81 80 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑄 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
82 81 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 1r ‘ 𝑄 ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
83 61 77 82 3eqtr4d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ( .r ‘ ( oppr ‘ 𝑄 ) ) 𝑢 ) = ( 1r ‘ 𝑄 ) )
84 60 83 eqtr3id ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) )
85 29 26 25 30 31 35 38 48 51 57 84 ringinveu ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) )
86 85 67 52 3eqtr4rd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑣 = 𝑤 )
87 86 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 𝑢 ( .r ‘ 𝑄 ) 𝑤 ) )
88 67 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑤 ) = ( 𝑢 ( .r ‘ 𝑄 ) [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) )
89 87 88 84 3eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) )
90 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
91 71 qseq2d ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( ( Base ‘ 𝑅 ) / ( 𝑂 ~QG 𝑀 ) ) )
92 91 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( ( Base ‘ 𝑅 ) / ( 𝑂 ~QG 𝑀 ) ) )
93 eqidd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) )
94 1 6 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
95 94 a1i ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
96 ovexd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑂 ~QG 𝑀 ) ∈ V )
97 1 fvexi ⊢ 𝑂 ∈ V
98 97 a1i ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑂 ∈ V )
99 93 95 96 98 qusbas ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑂 ~QG 𝑀 ) ) = ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
100 92 99 eqtr2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) = ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
101 90 100 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑤 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
102 elqsi ⊢ ( 𝑤 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑠 ∈ ( Base ‘ 𝑅 ) 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
103 101 102 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑠 ∈ ( Base ‘ 𝑅 ) 𝑤 = [ 𝑠 ] ( 𝑅 ~QG 𝑀 ) )
104 89 103 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) )
105 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) → 𝑣 ∈ ( Base ‘ 𝑄 ) )
106 46 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) → ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) = ( Base ‘ 𝑄 ) )
107 105 106 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) → 𝑣 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
108 elqsi ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑟 ∈ ( Base ‘ 𝑅 ) 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) )
109 107 108 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) → ∃ 𝑟 ∈ ( Base ‘ 𝑅 ) 𝑣 = [ 𝑟 ] ( 𝑅 ~QG 𝑀 ) )
110 104 109 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ∧ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) ∧ ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) )
111 eqid ⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
112 eqid ⊢ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) = ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) )
113 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑅 ∈ NzRing )
114 1 opprnzr ⊢ ( 𝑅 ∈ NzRing → 𝑂 ∈ NzRing )
115 113 114 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑂 ∈ NzRing )
116 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑂 ) )
117 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
118 1 62 117 opprmxidlabs ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑂 ) ) )
119 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
120 94 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
121 119 120 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → 𝑥 ∈ ( Base ‘ 𝑂 ) )
122 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) )
123 8 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
124 123 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ Grp )
125 lidlnsg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) )
126 8 10 125 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) )
127 nsgsubg ⊢ ( 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
128 126 127 syl ⊢ ( 𝜑 → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
129 128 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → 𝑀 ∈ ( SubGrp ‘ 𝑅 ) )
130 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ∈ 𝑀 )
131 eqid ⊢ ( 𝑅 ~QG 𝑀 ) = ( 𝑅 ~QG 𝑀 )
132 131 eqg0el ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑀 ∈ ( SubGrp ‘ 𝑅 ) ) → ( [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = 𝑀 ↔ 𝑥 ∈ 𝑀 ) )
133 132 biimpar ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝑀 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑀 ) → [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = 𝑀 )
134 124 129 130 133 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = 𝑀 )
135 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
136 6 131 135 eqgid ⊢ ( 𝑀 ∈ ( SubGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = 𝑀 )
137 129 136 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = 𝑀 )
138 134 137 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) = [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) )
139 2 135 qus0 ⊢ ( 𝑀 ∈ ( NrmSGrp ‘ 𝑅 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 0g ‘ 𝑄 ) )
140 126 139 syl ⊢ ( 𝜑 → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 0g ‘ 𝑄 ) )
141 140 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → [ ( 0g ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑀 ) = ( 0g ‘ 𝑄 ) )
142 122 138 141 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → 𝑢 = ( 0g ‘ 𝑄 ) )
143 eldifsnneq ⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) → ¬ 𝑢 = ( 0g ‘ 𝑄 ) )
144 143 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑥 ∈ 𝑀 ) → ¬ 𝑢 = ( 0g ‘ 𝑄 ) )
145 142 144 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → ¬ 𝑥 ∈ 𝑀 )
146 111 112 115 116 118 121 145 qsdrngilem ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
147 146 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) ( 𝑤 ( .r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) [ 𝑥 ] ( 𝑂 ~QG 𝑀 ) ) = ( 1r ‘ ( 𝑂 /s ( 𝑂 ~QG 𝑀 ) ) ) )
148 110 147 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) )
149 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) )
150 149 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) )
151 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) )
152 150 151 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) )
153 148 152 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ 𝑣 ∈ ( Base ‘ 𝑄 ) ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) → ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) )
154 153 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) ∧ ( 𝑣 ∈ ( Base ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) ) ) → ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) )
155 1 2 113 117 116 119 145 qsdrngilem ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( 𝑣 ( .r ‘ 𝑄 ) [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) = ( 1r ‘ 𝑄 ) )
156 154 155 reximddv ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) )
157 37 46 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → 𝑢 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) )
158 elqsi ⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑅 ) / ( 𝑅 ~QG 𝑀 ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) )
159 157 158 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑢 = [ 𝑥 ] ( 𝑅 ~QG 𝑀 ) )
160 156 159 r19.29a ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ) → ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) )
161 160 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) )
162 29 26 25 30 31 33 isdrng4 ⊢ ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( ( 1r ‘ 𝑄 ) ≠ ( 0g ‘ 𝑄 ) ∧ ∀ 𝑢 ∈ ( ( Base ‘ 𝑄 ) ∖ { ( 0g ‘ 𝑄 ) } ) ∃ 𝑣 ∈ ( Base ‘ 𝑄 ) ( ( 𝑢 ( .r ‘ 𝑄 ) 𝑣 ) = ( 1r ‘ 𝑄 ) ∧ ( 𝑣 ( .r ‘ 𝑄 ) 𝑢 ) = ( 1r ‘ 𝑄 ) ) ) ) )
163 28 161 162 mpbir2and ⊢ ( 𝜑 → 𝑄 ∈ DivRing )