Metamath Proof Explorer

Theorem zarcmplem

Description: Lemma for zarcmp . (Contributed by Thierry Arnoux, 2-Jul-2024)

Ref Expression
Hypotheses zartop.1 
|- S = ( Spec ` R )
zartop.2 
|- J = ( TopOpen ` S )
zarcmplem.1 
|- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
Assertion zarcmplem 
|- ( R e. CRing -> J e. Comp )

Proof

Step Hyp Ref Expression
1 zartop.1 
 |-  S = ( Spec ` R )
2 zartop.2 
 |-  J = ( TopOpen ` S )
3 zarcmplem.1 
 |-  V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } )
4 crngring 
 |-  ( R e. CRing -> R e. Ring )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 1 2 5 zar0ring 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> J = { (/) } )
7 4 6 sylan 
 |-  ( ( R e. CRing /\ ( # ` ( Base ` R ) ) = 1 ) -> J = { (/) } )
8 0cmp 
 |-  { (/) } e. Comp
9 7 8 eqeltrdi 
 |-  ( ( R e. CRing /\ ( # ` ( Base ` R ) ) = 1 ) -> J e. Comp )
10 1 2 zartop 
 |-  ( R e. CRing -> J e. Top )
11 fvex 
 |-  ( LIdeal ` R ) e. _V
12 11 mptex 
 |-  ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) e. _V
13 3 12 eqeltri 
 |-  V e. _V
14 imaexg 
 |-  ( V e. _V -> ( V " ( a supp ( 0g ` R ) ) ) e. _V )
15 13 14 mp1i 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) e. _V )
16 suppssdm 
 |-  ( a supp ( 0g ` R ) ) C_ dom a
17 imass2 
 |-  ( ( a supp ( 0g ` R ) ) C_ dom a -> ( V " ( a supp ( 0g ` R ) ) ) C_ ( V " dom a ) )
18 16 17 mp1i 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) C_ ( V " dom a ) )
19 3 funmpt2 
 |-  Fun V
20 ssidd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> dom a C_ dom a )
21 simpllr 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> a e. ( ( Base ` R ) ^m ( `' V " x ) ) )
22 fvexd 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> ( Base ` R ) e. _V )
23 13 cnvex 
 |-  `' V e. _V
24 23 imaex 
 |-  ( `' V " x ) e. _V
25 24 a1i 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> ( `' V " x ) e. _V )
26 22 25 elmapd 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> ( a e. ( ( Base ` R ) ^m ( `' V " x ) ) <-> a : ( `' V " x ) --> ( Base ` R ) ) )
27 21 26 mpbid 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> a : ( `' V " x ) --> ( Base ` R ) )
28 27 fdmd 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> dom a = ( `' V " x ) )
29 28 adantr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> dom a = ( `' V " x ) )
30 20 29 sseqtrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> dom a C_ ( `' V " x ) )
31 funimass2 
 |-  ( ( Fun V /\ dom a C_ ( `' V " x ) ) -> ( V " dom a ) C_ x )
32 19 30 31 sylancr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " dom a ) C_ x )
33 18 32 sstrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) C_ x )
34 15 33 elpwd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) e. ~P x )
35 simpllr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> a finSupp ( 0g ` R ) )
36 35 fsuppimpd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) e. Fin )
37 imafi 
 |-  ( ( Fun V /\ ( a supp ( 0g ` R ) ) e. Fin ) -> ( V " ( a supp ( 0g ` R ) ) ) e. Fin )
38 19 36 37 sylancr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) e. Fin )
39 34 38 elind 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V " ( a supp ( 0g ` R ) ) ) e. ( ~P x i^i Fin ) )
40 inteq 
 |-  ( y = ( V " ( a supp ( 0g ` R ) ) ) -> |^| y = |^| ( V " ( a supp ( 0g ` R ) ) ) )
41 40 eqeq2d 
 |-  ( y = ( V " ( a supp ( 0g ` R ) ) ) -> ( (/) = |^| y <-> (/) = |^| ( V " ( a supp ( 0g ` R ) ) ) ) )
42 41 adantl 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ y = ( V " ( a supp ( 0g ` R ) ) ) ) -> ( (/) = |^| y <-> (/) = |^| ( V " ( a supp ( 0g ` R ) ) ) ) )
43 16 29 sseqtrid 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) C_ ( `' V " x ) )
44 cnvimass 
 |-  ( `' V " x ) C_ dom V
45 43 44 sstrdi 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) C_ dom V )
46 intimafv 
 |-  ( ( Fun V /\ ( a supp ( 0g ` R ) ) C_ dom V ) -> |^| ( V " ( a supp ( 0g ` R ) ) ) = |^|_ l e. ( a supp ( 0g ` R ) ) ( V ` l ) )
47 19 45 46 sylancr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> |^| ( V " ( a supp ( 0g ` R ) ) ) = |^|_ l e. ( a supp ( 0g ` R ) ) ( V ` l ) )
48 simplll 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> R e. CRing )
49 48 crngringd 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> R e. Ring )
50 49 ad4antr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> R e. Ring )
51 fvex 
 |-  ( PrmIdeal ` R ) e. _V
52 51 rabex 
 |-  { j e. ( PrmIdeal ` R ) | i C_ j } e. _V
53 52 3 dmmpti 
 |-  dom V = ( LIdeal ` R )
54 45 53 sseqtrdi 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) C_ ( LIdeal ` R ) )
55 simp-7r 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( # ` ( Base ` R ) ) =/= 1 )
56 simpllr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( 1r ` R ) = ( R gsum a ) )
57 res0 
 |-  ( a |` (/) ) = (/)
58 57 oveq2i 
 |-  ( R gsum ( a |` (/) ) ) = ( R gsum (/) )
59 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
60 59 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
61 58 60 eqtri 
 |-  ( R gsum ( a |` (/) ) ) = ( 0g ` R )
62 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
63 4 62 syl 
 |-  ( R e. CRing -> R e. CMnd )
64 63 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> R e. CMnd )
65 24 a1i 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( `' V " x ) e. _V )
66 27 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> a : ( `' V " x ) --> ( Base ` R ) )
67 simpr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( a supp ( 0g ` R ) ) = (/) )
68 ssidd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> (/) C_ (/) )
69 67 68 eqsstrd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( a supp ( 0g ` R ) ) C_ (/) )
70 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> a finSupp ( 0g ` R ) )
71 5 59 64 65 66 69 70 gsumres 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( R gsum ( a |` (/) ) ) = ( R gsum a ) )
72 61 71 syl5reqr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( R gsum a ) = ( 0g ` R ) )
73 56 72 eqtr2d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( 0g ` R ) = ( 1r ` R ) )
74 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
75 5 59 74 01eq0ring 
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> ( Base ` R ) = { ( 0g ` R ) } )
76 50 73 75 syl2an2r 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( Base ` R ) = { ( 0g ` R ) } )
77 76 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( # ` ( Base ` R ) ) = ( # ` { ( 0g ` R ) } ) )
78 fvex 
 |-  ( 0g ` R ) e. _V
79 hashsng 
 |-  ( ( 0g ` R ) e. _V -> ( # ` { ( 0g ` R ) } ) = 1 )
80 78 79 ax-mp 
 |-  ( # ` { ( 0g ` R ) } ) = 1
81 77 80 eqtrdi 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ ( a supp ( 0g ` R ) ) = (/) ) -> ( # ` ( Base ` R ) ) = 1 )
82 55 81 mteqand 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) =/= (/) )
83 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
84 3 83 zarclsiin 
 |-  ( ( R e. Ring /\ ( a supp ( 0g ` R ) ) C_ ( LIdeal ` R ) /\ ( a supp ( 0g ` R ) ) =/= (/) ) -> |^|_ l e. ( a supp ( 0g ` R ) ) ( V ` l ) = ( V ` ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) ) )
85 50 54 82 84 syl3anc 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> |^|_ l e. ( a supp ( 0g ` R ) ) ( V ` l ) = ( V ` ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) ) )
86 nfv 
 |-  F/ l ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) )
87 nfra1 
 |-  F/ l A. l e. ( `' V " x ) ( a ` l ) e. l
88 86 87 nfan 
 |-  F/ l ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l )
89 54 sselda 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ l e. ( a supp ( 0g ` R ) ) ) -> l e. ( LIdeal ` R ) )
90 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
91 5 90 lidlss 
 |-  ( l e. ( LIdeal ` R ) -> l C_ ( Base ` R ) )
92 89 91 syl 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ l e. ( a supp ( 0g ` R ) ) ) -> l C_ ( Base ` R ) )
93 92 ex 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( l e. ( a supp ( 0g ` R ) ) -> l C_ ( Base ` R ) ) )
94 88 93 ralrimi 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> A. l e. ( a supp ( 0g ` R ) ) l C_ ( Base ` R ) )
95 unissb 
 |-  ( U. ( a supp ( 0g ` R ) ) C_ ( Base ` R ) <-> A. l e. ( a supp ( 0g ` R ) ) l C_ ( Base ` R ) )
96 94 95 sylibr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> U. ( a supp ( 0g ` R ) ) C_ ( Base ` R ) )
97 83 5 90 rspcl 
 |-  ( ( R e. Ring /\ U. ( a supp ( 0g ` R ) ) C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) e. ( LIdeal ` R ) )
98 50 96 97 syl2anc 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) e. ( LIdeal ` R ) )
99 5 90 lidlss 
 |-  ( ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) e. ( LIdeal ` R ) -> ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) C_ ( Base ` R ) )
100 98 99 syl 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) C_ ( Base ` R ) )
101 83 5 74 rsp1 
 |-  ( R e. Ring -> ( ( RSpan ` R ) ` { ( 1r ` R ) } ) = ( Base ` R ) )
102 50 101 syl 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( RSpan ` R ) ` { ( 1r ` R ) } ) = ( Base ` R ) )
103 27 adantr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> a : ( `' V " x ) --> ( Base ` R ) )
104 103 43 fssresd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a |` ( a supp ( 0g ` R ) ) ) : ( a supp ( 0g ` R ) ) --> ( Base ` R ) )
105 fvex 
 |-  ( Base ` R ) e. _V
106 ovex 
 |-  ( a supp ( 0g ` R ) ) e. _V
107 105 106 elmap 
 |-  ( ( a |` ( a supp ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m ( a supp ( 0g ` R ) ) ) <-> ( a |` ( a supp ( 0g ` R ) ) ) : ( a supp ( 0g ` R ) ) --> ( Base ` R ) )
108 104 107 sylibr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a |` ( a supp ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m ( a supp ( 0g ` R ) ) ) )
109 breq1 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( b finSupp ( 0g ` R ) <-> ( a |` ( a supp ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) )
110 oveq2 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( R gsum b ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) )
111 110 eqeq2d 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( ( 1r ` R ) = ( R gsum b ) <-> ( 1r ` R ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) ) )
112 fveq1 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( b ` k ) = ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) )
113 112 eleq1d 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( ( b ` k ) e. k <-> ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k ) )
114 113 ralbidv 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( A. k e. ( a supp ( 0g ` R ) ) ( b ` k ) e. k <-> A. k e. ( a supp ( 0g ` R ) ) ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k ) )
115 109 111 114 3anbi123d 
 |-  ( b = ( a |` ( a supp ( 0g ` R ) ) ) -> ( ( b finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum b ) /\ A. k e. ( a supp ( 0g ` R ) ) ( b ` k ) e. k ) <-> ( ( a |` ( a supp ( 0g ` R ) ) ) finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) /\ A. k e. ( a supp ( 0g ` R ) ) ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k ) ) )
116 115 adantl 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ b = ( a |` ( a supp ( 0g ` R ) ) ) ) -> ( ( b finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum b ) /\ A. k e. ( a supp ( 0g ` R ) ) ( b ` k ) e. k ) <-> ( ( a |` ( a supp ( 0g ` R ) ) ) finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) /\ A. k e. ( a supp ( 0g ` R ) ) ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k ) ) )
117 fvexd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( 0g ` R ) e. _V )
118 35 117 fsuppres 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a |` ( a supp ( 0g ` R ) ) ) finSupp ( 0g ` R ) )
119 simplr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( 1r ` R ) = ( R gsum a ) )
120 50 62 syl 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> R e. CMnd )
121 24 a1i 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( `' V " x ) e. _V )
122 ssidd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a supp ( 0g ` R ) ) C_ ( a supp ( 0g ` R ) ) )
123 5 59 120 121 103 122 35 gsumres 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) = ( R gsum a ) )
124 119 123 eqtr4d 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( 1r ` R ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) )
125 simpr 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ k e. ( a supp ( 0g ` R ) ) ) -> k e. ( a supp ( 0g ` R ) ) )
126 125 fvresd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ k e. ( a supp ( 0g ` R ) ) ) -> ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) = ( a ` k ) )
127 16 28 sseqtrid 
 |-  ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) -> ( a supp ( 0g ` R ) ) C_ ( `' V " x ) )
128 127 sselda 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ k e. ( a supp ( 0g ` R ) ) ) -> k e. ( `' V " x ) )
129 fveq2 
 |-  ( l = k -> ( a ` l ) = ( a ` k ) )
130 id 
 |-  ( l = k -> l = k )
131 129 130 eleq12d 
 |-  ( l = k -> ( ( a ` l ) e. l <-> ( a ` k ) e. k ) )
132 131 adantl 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ k e. ( a supp ( 0g ` R ) ) ) /\ l = k ) -> ( ( a ` l ) e. l <-> ( a ` k ) e. k ) )
133 128 132 rspcdv 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ k e. ( a supp ( 0g ` R ) ) ) -> ( A. l e. ( `' V " x ) ( a ` l ) e. l -> ( a ` k ) e. k ) )
134 133 imp 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ k e. ( a supp ( 0g ` R ) ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( a ` k ) e. k )
135 134 an32s 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ k e. ( a supp ( 0g ` R ) ) ) -> ( a ` k ) e. k )
136 126 135 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) /\ k e. ( a supp ( 0g ` R ) ) ) -> ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k )
137 136 ralrimiva 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> A. k e. ( a supp ( 0g ` R ) ) ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k )
138 118 124 137 3jca 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( a |` ( a supp ( 0g ` R ) ) ) finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum ( a |` ( a supp ( 0g ` R ) ) ) ) /\ A. k e. ( a supp ( 0g ` R ) ) ( ( a |` ( a supp ( 0g ` R ) ) ) ` k ) e. k ) )
139 108 116 138 rspcedvd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> E. b e. ( ( Base ` R ) ^m ( a supp ( 0g ` R ) ) ) ( b finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum b ) /\ A. k e. ( a supp ( 0g ` R ) ) ( b ` k ) e. k ) )
140 eqid 
 |-  ( .r ` R ) = ( .r ` R )
141 83 5 59 140 50 54 elrspunidl 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( 1r ` R ) e. ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) <-> E. b e. ( ( Base ` R ) ^m ( a supp ( 0g ` R ) ) ) ( b finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum b ) /\ A. k e. ( a supp ( 0g ` R ) ) ( b ` k ) e. k ) ) )
142 139 141 mpbird 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( 1r ` R ) e. ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) )
143 142 snssd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> { ( 1r ` R ) } C_ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) )
144 83 90 rspssp 
 |-  ( ( R e. Ring /\ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) e. ( LIdeal ` R ) /\ { ( 1r ` R ) } C_ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) ) -> ( ( RSpan ` R ) ` { ( 1r ` R ) } ) C_ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) )
145 50 98 143 144 syl3anc 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( RSpan ` R ) ` { ( 1r ` R ) } ) C_ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) )
146 102 145 eqsstrrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( Base ` R ) C_ ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) )
147 100 146 eqssd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) = ( Base ` R ) )
148 147 fveq2d 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V ` ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) ) = ( V ` ( Base ` R ) ) )
149 90 5 lidl1 
 |-  ( R e. Ring -> ( Base ` R ) e. ( LIdeal ` R ) )
150 4 149 syl 
 |-  ( R e. CRing -> ( Base ` R ) e. ( LIdeal ` R ) )
151 3 5 zarcls1 
 |-  ( ( R e. CRing /\ ( Base ` R ) e. ( LIdeal ` R ) ) -> ( ( V ` ( Base ` R ) ) = (/) <-> ( Base ` R ) = ( Base ` R ) ) )
152 150 151 mpdan 
 |-  ( R e. CRing -> ( ( V ` ( Base ` R ) ) = (/) <-> ( Base ` R ) = ( Base ` R ) ) )
153 5 152 mpbiri 
 |-  ( R e. CRing -> ( V ` ( Base ` R ) ) = (/) )
154 153 ad7antr 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V ` ( Base ` R ) ) = (/) )
155 148 154 eqtrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> ( V ` ( ( RSpan ` R ) ` U. ( a supp ( 0g ` R ) ) ) ) = (/) )
156 47 85 155 3eqtrrd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> (/) = |^| ( V " ( a supp ( 0g ` R ) ) ) )
157 39 42 156 rspcedvd 
 |-  ( ( ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ a finSupp ( 0g ` R ) ) /\ ( 1r ` R ) = ( R gsum a ) ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) -> E. y e. ( ~P x i^i Fin ) (/) = |^| y )
158 157 exp41 
 |-  ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) -> ( a finSupp ( 0g ` R ) -> ( ( 1r ` R ) = ( R gsum a ) -> ( A. l e. ( `' V " x ) ( a ` l ) e. l -> E. y e. ( ~P x i^i Fin ) (/) = |^| y ) ) ) )
159 158 3imp2 
 |-  ( ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ a e. ( ( Base ` R ) ^m ( `' V " x ) ) ) /\ ( a finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum a ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) ) -> E. y e. ( ~P x i^i Fin ) (/) = |^| y )
160 5 74 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
161 49 160 syl 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( 1r ` R ) e. ( Base ` R ) )
162 simplr 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> x e. ~P ( Clsd ` J ) )
163 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
164 1 2 163 3 zartopn 
 |-  ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran V = ( Clsd ` J ) ) )
165 164 simprd 
 |-  ( R e. CRing -> ran V = ( Clsd ` J ) )
166 48 165 syl 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ran V = ( Clsd ` J ) )
167 166 pweqd 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ~P ran V = ~P ( Clsd ` J ) )
168 162 167 eleqtrrd 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> x e. ~P ran V )
169 168 elpwid 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> x C_ ran V )
170 intimafv 
 |-  ( ( Fun V /\ ( `' V " x ) C_ dom V ) -> |^| ( V " ( `' V " x ) ) = |^|_ l e. ( `' V " x ) ( V ` l ) )
171 19 44 170 mp2an 
 |-  |^| ( V " ( `' V " x ) ) = |^|_ l e. ( `' V " x ) ( V ` l )
172 funimacnv 
 |-  ( Fun V -> ( V " ( `' V " x ) ) = ( x i^i ran V ) )
173 19 172 ax-mp 
 |-  ( V " ( `' V " x ) ) = ( x i^i ran V )
174 df-ss 
 |-  ( x C_ ran V <-> ( x i^i ran V ) = x )
175 174 biimpi 
 |-  ( x C_ ran V -> ( x i^i ran V ) = x )
176 173 175 syl5eq 
 |-  ( x C_ ran V -> ( V " ( `' V " x ) ) = x )
177 176 inteqd 
 |-  ( x C_ ran V -> |^| ( V " ( `' V " x ) ) = |^| x )
178 171 177 eqtr3id 
 |-  ( x C_ ran V -> |^|_ l e. ( `' V " x ) ( V ` l ) = |^| x )
179 169 178 syl 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> |^|_ l e. ( `' V " x ) ( V ` l ) = |^| x )
180 44 a1i 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( `' V " x ) C_ dom V )
181 180 53 sseqtrdi 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( `' V " x ) C_ ( LIdeal ` R ) )
182 19 a1i 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> Fun V )
183 inteq 
 |-  ( x = (/) -> |^| x = |^| (/) )
184 int0 
 |-  |^| (/) = _V
185 183 184 eqtrdi 
 |-  ( x = (/) -> |^| x = _V )
186 vn0 
 |-  _V =/= (/)
187 neeq1 
 |-  ( |^| x = _V -> ( |^| x =/= (/) <-> _V =/= (/) ) )
188 186 187 mpbiri 
 |-  ( |^| x = _V -> |^| x =/= (/) )
189 185 188 syl 
 |-  ( x = (/) -> |^| x =/= (/) )
190 189 necon2i 
 |-  ( |^| x = (/) -> x =/= (/) )
191 190 adantl 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> x =/= (/) )
192 preiman0 
 |-  ( ( Fun V /\ x C_ ran V /\ x =/= (/) ) -> ( `' V " x ) =/= (/) )
193 182 169 191 192 syl3anc 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( `' V " x ) =/= (/) )
194 3 83 zarclsiin 
 |-  ( ( R e. Ring /\ ( `' V " x ) C_ ( LIdeal ` R ) /\ ( `' V " x ) =/= (/) ) -> |^|_ l e. ( `' V " x ) ( V ` l ) = ( V ` ( ( RSpan ` R ) ` U. ( `' V " x ) ) ) )
195 49 181 193 194 syl3anc 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> |^|_ l e. ( `' V " x ) ( V ` l ) = ( V ` ( ( RSpan ` R ) ` U. ( `' V " x ) ) ) )
196 simpr 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> |^| x = (/) )
197 179 195 196 3eqtr3d 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( V ` ( ( RSpan ` R ) ` U. ( `' V " x ) ) ) = (/) )
198 181 sselda 
 |-  ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ l e. ( `' V " x ) ) -> l e. ( LIdeal ` R ) )
199 198 91 syl 
 |-  ( ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) /\ l e. ( `' V " x ) ) -> l C_ ( Base ` R ) )
200 199 ralrimiva 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> A. l e. ( `' V " x ) l C_ ( Base ` R ) )
201 unissb 
 |-  ( U. ( `' V " x ) C_ ( Base ` R ) <-> A. l e. ( `' V " x ) l C_ ( Base ` R ) )
202 200 201 sylibr 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> U. ( `' V " x ) C_ ( Base ` R ) )
203 83 5 90 rspcl 
 |-  ( ( R e. Ring /\ U. ( `' V " x ) C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` U. ( `' V " x ) ) e. ( LIdeal ` R ) )
204 49 202 203 syl2anc 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( ( RSpan ` R ) ` U. ( `' V " x ) ) e. ( LIdeal ` R ) )
205 3 5 zarcls1 
 |-  ( ( R e. CRing /\ ( ( RSpan ` R ) ` U. ( `' V " x ) ) e. ( LIdeal ` R ) ) -> ( ( V ` ( ( RSpan ` R ) ` U. ( `' V " x ) ) ) = (/) <-> ( ( RSpan ` R ) ` U. ( `' V " x ) ) = ( Base ` R ) ) )
206 48 204 205 syl2anc 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( ( V ` ( ( RSpan ` R ) ` U. ( `' V " x ) ) ) = (/) <-> ( ( RSpan ` R ) ` U. ( `' V " x ) ) = ( Base ` R ) ) )
207 197 206 mpbid 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( ( RSpan ` R ) ` U. ( `' V " x ) ) = ( Base ` R ) )
208 161 207 eleqtrrd 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( 1r ` R ) e. ( ( RSpan ` R ) ` U. ( `' V " x ) ) )
209 83 5 59 140 49 181 elrspunidl 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> ( ( 1r ` R ) e. ( ( RSpan ` R ) ` U. ( `' V " x ) ) <-> E. a e. ( ( Base ` R ) ^m ( `' V " x ) ) ( a finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum a ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) ) )
210 208 209 mpbid 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> E. a e. ( ( Base ` R ) ^m ( `' V " x ) ) ( a finSupp ( 0g ` R ) /\ ( 1r ` R ) = ( R gsum a ) /\ A. l e. ( `' V " x ) ( a ` l ) e. l ) )
211 159 210 r19.29a 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> E. y e. ( ~P x i^i Fin ) (/) = |^| y )
212 0ex 
 |-  (/) e. _V
213 vex 
 |-  x e. _V
214 elfi 
 |-  ( ( (/) e. _V /\ x e. _V ) -> ( (/) e. ( fi ` x ) <-> E. y e. ( ~P x i^i Fin ) (/) = |^| y ) )
215 212 213 214 mp2an 
 |-  ( (/) e. ( fi ` x ) <-> E. y e. ( ~P x i^i Fin ) (/) = |^| y )
216 211 215 sylibr 
 |-  ( ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) /\ |^| x = (/) ) -> (/) e. ( fi ` x ) )
217 216 ex 
 |-  ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) -> ( |^| x = (/) -> (/) e. ( fi ` x ) ) )
218 217 necon3bd 
 |-  ( ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) /\ x e. ~P ( Clsd ` J ) ) -> ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) )
219 218 ralrimiva 
 |-  ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) -> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) )
220 cmpfi 
 |-  ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )
221 220 biimpar 
 |-  ( ( J e. Top /\ A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) -> J e. Comp )
222 10 219 221 syl2an2r 
 |-  ( ( R e. CRing /\ ( # ` ( Base ` R ) ) =/= 1 ) -> J e. Comp )
223 9 222 pm2.61dane 
 |-  ( R e. CRing -> J e. Comp )