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

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 
|- O = ( oppR ` R )
qsdrng.q 
|- Q = ( R /s ( R ~QG M ) )
qsdrng.r 
|- ( ph -> R e. NzRing )
qsdrngi.1 
|- ( ph -> M e. ( MaxIdeal ` R ) )
qsdrngi.2 
|- ( ph -> M e. ( MaxIdeal ` O ) )
Assertion qsdrngi 
|- ( ph -> Q e. DivRing )

Proof

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