Metamath Proof Explorer

Theorem rprmdvdsprod

Description: If a prime element Q divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmdvdsprod.b 
|- B = ( Base ` R )
rprmdvdsprod.p 
|- P = ( RPrime ` R )
rprmdvdsprod.d 
|- .|| = ( ||r ` R )
rprmdvdsprod.1 
|- .1. = ( 1r ` R )
rprmdvdsprod.m 
|- M = ( mulGrp ` R )
rprmdvdsprod.r 
|- ( ph -> R e. CRing )
rprmdvdsprod.q 
|- ( ph -> Q e. P )
rprmdvdsprod.i 
|- ( ph -> I e. V )
rprmdvdsprod.2 
|- ( ph -> F finSupp .1. )
rprmdvdsprod.f 
|- ( ph -> F : I --> B )
rprmdvdsprod.3 
|- ( ph -> Q .|| ( M gsum F ) )
Assertion rprmdvdsprod 
|- ( ph -> E. x e. ( F supp .1. ) Q .|| ( F ` x ) )

Proof

Step Hyp Ref Expression
1 rprmdvdsprod.b 
 |-  B = ( Base ` R )
2 rprmdvdsprod.p 
 |-  P = ( RPrime ` R )
3 rprmdvdsprod.d 
 |-  .|| = ( ||r ` R )
4 rprmdvdsprod.1 
 |-  .1. = ( 1r ` R )
5 rprmdvdsprod.m 
 |-  M = ( mulGrp ` R )
6 rprmdvdsprod.r 
 |-  ( ph -> R e. CRing )
7 rprmdvdsprod.q 
 |-  ( ph -> Q e. P )
8 rprmdvdsprod.i 
 |-  ( ph -> I e. V )
9 rprmdvdsprod.2 
 |-  ( ph -> F finSupp .1. )
10 rprmdvdsprod.f 
 |-  ( ph -> F : I --> B )
11 rprmdvdsprod.3 
 |-  ( ph -> Q .|| ( M gsum F ) )
12 5 1 mgpbas 
 |-  B = ( Base ` M )
13 5 4 ringidval 
 |-  .1. = ( 0g ` M )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 5 14 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
16 5 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
17 6 16 syl 
 |-  ( ph -> M e. CMnd )
18 disjdifr 
 |-  ( ( I \ ( F supp .1. ) ) i^i ( F supp .1. ) ) = (/)
19 18 a1i 
 |-  ( ph -> ( ( I \ ( F supp .1. ) ) i^i ( F supp .1. ) ) = (/) )
20 suppssdm 
 |-  ( F supp .1. ) C_ dom F
21 20 10 fssdm 
 |-  ( ph -> ( F supp .1. ) C_ I )
22 undifr 
 |-  ( ( F supp .1. ) C_ I <-> ( ( I \ ( F supp .1. ) ) u. ( F supp .1. ) ) = I )
23 21 22 sylib 
 |-  ( ph -> ( ( I \ ( F supp .1. ) ) u. ( F supp .1. ) ) = I )
24 23 eqcomd 
 |-  ( ph -> I = ( ( I \ ( F supp .1. ) ) u. ( F supp .1. ) ) )
25 12 13 15 17 8 10 9 19 24 gsumsplit 
 |-  ( ph -> ( M gsum F ) = ( ( M gsum ( F |` ( I \ ( F supp .1. ) ) ) ) ( .r ` R ) ( M gsum ( F |` ( F supp .1. ) ) ) ) )
26 difssd 
 |-  ( ph -> ( I \ ( F supp .1. ) ) C_ I )
27 10 26 feqresmpt 
 |-  ( ph -> ( F |` ( I \ ( F supp .1. ) ) ) = ( z e. ( I \ ( F supp .1. ) ) |-> ( F ` z ) ) )
28 10 ffnd 
 |-  ( ph -> F Fn I )
29 28 adantr 
 |-  ( ( ph /\ z e. ( I \ ( F supp .1. ) ) ) -> F Fn I )
30 8 adantr 
 |-  ( ( ph /\ z e. ( I \ ( F supp .1. ) ) ) -> I e. V )
31 6 crngringd 
 |-  ( ph -> R e. Ring )
32 1 4 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
33 31 32 syl 
 |-  ( ph -> .1. e. B )
34 33 adantr 
 |-  ( ( ph /\ z e. ( I \ ( F supp .1. ) ) ) -> .1. e. B )
35 simpr 
 |-  ( ( ph /\ z e. ( I \ ( F supp .1. ) ) ) -> z e. ( I \ ( F supp .1. ) ) )
36 29 30 34 35 fvdifsupp 
 |-  ( ( ph /\ z e. ( I \ ( F supp .1. ) ) ) -> ( F ` z ) = .1. )
37 36 mpteq2dva 
 |-  ( ph -> ( z e. ( I \ ( F supp .1. ) ) |-> ( F ` z ) ) = ( z e. ( I \ ( F supp .1. ) ) |-> .1. ) )
38 27 37 eqtrd 
 |-  ( ph -> ( F |` ( I \ ( F supp .1. ) ) ) = ( z e. ( I \ ( F supp .1. ) ) |-> .1. ) )
39 38 oveq2d 
 |-  ( ph -> ( M gsum ( F |` ( I \ ( F supp .1. ) ) ) ) = ( M gsum ( z e. ( I \ ( F supp .1. ) ) |-> .1. ) ) )
40 17 cmnmndd 
 |-  ( ph -> M e. Mnd )
41 8 difexd 
 |-  ( ph -> ( I \ ( F supp .1. ) ) e. _V )
42 13 gsumz 
 |-  ( ( M e. Mnd /\ ( I \ ( F supp .1. ) ) e. _V ) -> ( M gsum ( z e. ( I \ ( F supp .1. ) ) |-> .1. ) ) = .1. )
43 40 41 42 syl2anc 
 |-  ( ph -> ( M gsum ( z e. ( I \ ( F supp .1. ) ) |-> .1. ) ) = .1. )
44 39 43 eqtrd 
 |-  ( ph -> ( M gsum ( F |` ( I \ ( F supp .1. ) ) ) ) = .1. )
45 44 oveq1d 
 |-  ( ph -> ( ( M gsum ( F |` ( I \ ( F supp .1. ) ) ) ) ( .r ` R ) ( M gsum ( F |` ( F supp .1. ) ) ) ) = ( .1. ( .r ` R ) ( M gsum ( F |` ( F supp .1. ) ) ) ) )
46 ovexd 
 |-  ( ph -> ( F supp .1. ) e. _V )
47 10 21 fssresd 
 |-  ( ph -> ( F |` ( F supp .1. ) ) : ( F supp .1. ) --> B )
48 9 33 fsuppres 
 |-  ( ph -> ( F |` ( F supp .1. ) ) finSupp .1. )
49 12 13 17 46 47 48 gsumcl 
 |-  ( ph -> ( M gsum ( F |` ( F supp .1. ) ) ) e. B )
50 1 14 4 31 49 ringlidmd 
 |-  ( ph -> ( .1. ( .r ` R ) ( M gsum ( F |` ( F supp .1. ) ) ) ) = ( M gsum ( F |` ( F supp .1. ) ) ) )
51 25 45 50 3eqtrd 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( F |` ( F supp .1. ) ) ) )
52 11 51 breqtrd 
 |-  ( ph -> Q .|| ( M gsum ( F |` ( F supp .1. ) ) ) )
53 reseq2 
 |-  ( b = (/) -> ( F |` b ) = ( F |` (/) ) )
54 53 oveq2d 
 |-  ( b = (/) -> ( M gsum ( F |` b ) ) = ( M gsum ( F |` (/) ) ) )
55 54 breq2d 
 |-  ( b = (/) -> ( Q .|| ( M gsum ( F |` b ) ) <-> Q .|| ( M gsum ( F |` (/) ) ) ) )
56 rexeq 
 |-  ( b = (/) -> ( E. x e. b Q .|| ( F ` x ) <-> E. x e. (/) Q .|| ( F ` x ) ) )
57 55 56 imbi12d 
 |-  ( b = (/) -> ( ( Q .|| ( M gsum ( F |` b ) ) -> E. x e. b Q .|| ( F ` x ) ) <-> ( Q .|| ( M gsum ( F |` (/) ) ) -> E. x e. (/) Q .|| ( F ` x ) ) ) )
58 reseq2 
 |-  ( b = a -> ( F |` b ) = ( F |` a ) )
59 58 oveq2d 
 |-  ( b = a -> ( M gsum ( F |` b ) ) = ( M gsum ( F |` a ) ) )
60 59 breq2d 
 |-  ( b = a -> ( Q .|| ( M gsum ( F |` b ) ) <-> Q .|| ( M gsum ( F |` a ) ) ) )
61 rexeq 
 |-  ( b = a -> ( E. x e. b Q .|| ( F ` x ) <-> E. x e. a Q .|| ( F ` x ) ) )
62 60 61 imbi12d 
 |-  ( b = a -> ( ( Q .|| ( M gsum ( F |` b ) ) -> E. x e. b Q .|| ( F ` x ) ) <-> ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) )
63 reseq2 
 |-  ( b = ( a u. { y } ) -> ( F |` b ) = ( F |` ( a u. { y } ) ) )
64 63 oveq2d 
 |-  ( b = ( a u. { y } ) -> ( M gsum ( F |` b ) ) = ( M gsum ( F |` ( a u. { y } ) ) ) )
65 64 breq2d 
 |-  ( b = ( a u. { y } ) -> ( Q .|| ( M gsum ( F |` b ) ) <-> Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) )
66 rexeq 
 |-  ( b = ( a u. { y } ) -> ( E. x e. b Q .|| ( F ` x ) <-> E. x e. ( a u. { y } ) Q .|| ( F ` x ) ) )
67 65 66 imbi12d 
 |-  ( b = ( a u. { y } ) -> ( ( Q .|| ( M gsum ( F |` b ) ) -> E. x e. b Q .|| ( F ` x ) ) <-> ( Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) -> E. x e. ( a u. { y } ) Q .|| ( F ` x ) ) ) )
68 reseq2 
 |-  ( b = ( F supp .1. ) -> ( F |` b ) = ( F |` ( F supp .1. ) ) )
69 68 oveq2d 
 |-  ( b = ( F supp .1. ) -> ( M gsum ( F |` b ) ) = ( M gsum ( F |` ( F supp .1. ) ) ) )
70 69 breq2d 
 |-  ( b = ( F supp .1. ) -> ( Q .|| ( M gsum ( F |` b ) ) <-> Q .|| ( M gsum ( F |` ( F supp .1. ) ) ) ) )
71 rexeq 
 |-  ( b = ( F supp .1. ) -> ( E. x e. b Q .|| ( F ` x ) <-> E. x e. ( F supp .1. ) Q .|| ( F ` x ) ) )
72 70 71 imbi12d 
 |-  ( b = ( F supp .1. ) -> ( ( Q .|| ( M gsum ( F |` b ) ) -> E. x e. b Q .|| ( F ` x ) ) <-> ( Q .|| ( M gsum ( F |` ( F supp .1. ) ) ) -> E. x e. ( F supp .1. ) Q .|| ( F ` x ) ) ) )
73 4 3 2 6 7 rprmndvdsr1 
 |-  ( ph -> -. Q .|| .1. )
74 res0 
 |-  ( F |` (/) ) = (/)
75 74 oveq2i 
 |-  ( M gsum ( F |` (/) ) ) = ( M gsum (/) )
76 13 gsum0 
 |-  ( M gsum (/) ) = .1.
77 75 76 eqtri 
 |-  ( M gsum ( F |` (/) ) ) = .1.
78 77 a1i 
 |-  ( ph -> ( M gsum ( F |` (/) ) ) = .1. )
79 78 breq2d 
 |-  ( ph -> ( Q .|| ( M gsum ( F |` (/) ) ) <-> Q .|| .1. ) )
80 73 79 mtbird 
 |-  ( ph -> -. Q .|| ( M gsum ( F |` (/) ) ) )
81 80 pm2.21d 
 |-  ( ph -> ( Q .|| ( M gsum ( F |` (/) ) ) -> E. x e. (/) Q .|| ( F ` x ) ) )
82 simpllr 
 |-  ( ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) /\ Q .|| ( M gsum ( F |` a ) ) ) -> ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) )
83 82 syldbl2 
 |-  ( ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) /\ Q .|| ( M gsum ( F |` a ) ) ) -> E. x e. a Q .|| ( F ` x ) )
84 simpr 
 |-  ( ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) /\ Q .|| ( F ` y ) ) -> Q .|| ( F ` y ) )
85 vex 
 |-  y e. _V
86 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
87 86 breq2d 
 |-  ( x = y -> ( Q .|| ( F ` x ) <-> Q .|| ( F ` y ) ) )
88 85 87 rexsn 
 |-  ( E. x e. { y } Q .|| ( F ` x ) <-> Q .|| ( F ` y ) )
89 84 88 sylibr 
 |-  ( ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) /\ Q .|| ( F ` y ) ) -> E. x e. { y } Q .|| ( F ` x ) )
90 6 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> R e. CRing )
91 7 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> Q e. P )
92 90 16 syl 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> M e. CMnd )
93 vex 
 |-  a e. _V
94 93 a1i 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> a e. _V )
95 10 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> F : I --> B )
96 simp-4r 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> a C_ ( F supp .1. ) )
97 21 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F supp .1. ) C_ I )
98 96 97 sstrd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> a C_ I )
99 95 98 fssresd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F |` a ) : a --> B )
100 9 fsuppimpd 
 |-  ( ph -> ( F supp .1. ) e. Fin )
101 100 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F supp .1. ) e. Fin )
102 101 96 ssfid 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> a e. Fin )
103 33 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> .1. e. B )
104 99 102 103 fdmfifsupp 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F |` a ) finSupp .1. )
105 12 13 92 94 99 104 gsumcl 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( M gsum ( F |` a ) ) e. B )
106 97 ssdifssd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( ( F supp .1. ) \ a ) C_ I )
107 simpllr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> y e. ( ( F supp .1. ) \ a ) )
108 106 107 sseldd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> y e. I )
109 95 108 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F ` y ) e. B )
110 simpr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) )
111 eqid 
 |-  ( Cntz ` M ) = ( Cntz ` M )
112 eqid 
 |-  ( F ` y ) = ( F ` y )
113 40 ad4antr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> M e. Mnd )
114 107 eldifbd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> -. y e. a )
115 95 fimassd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F " ( a u. { y } ) ) C_ B )
116 12 111 cntzcmn 
 |-  ( ( M e. CMnd /\ ( F " ( a u. { y } ) ) C_ B ) -> ( ( Cntz ` M ) ` ( F " ( a u. { y } ) ) ) = B )
117 92 115 116 syl2anc 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( ( Cntz ` M ) ` ( F " ( a u. { y } ) ) ) = B )
118 115 117 sseqtrrd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( F " ( a u. { y } ) ) C_ ( ( Cntz ` M ) ` ( F " ( a u. { y } ) ) ) )
119 12 15 111 112 95 98 113 102 114 108 109 118 gsumzresunsn 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( M gsum ( F |` ( a u. { y } ) ) ) = ( ( M gsum ( F |` a ) ) ( .r ` R ) ( F ` y ) ) )
120 110 119 breqtrd 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> Q .|| ( ( M gsum ( F |` a ) ) ( .r ` R ) ( F ` y ) ) )
121 1 2 3 14 90 91 105 109 120 rprmdvds 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( Q .|| ( M gsum ( F |` a ) ) \/ Q .|| ( F ` y ) ) )
122 83 89 121 orim12da 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> ( E. x e. a Q .|| ( F ` x ) \/ E. x e. { y } Q .|| ( F ` x ) ) )
123 rexun 
 |-  ( E. x e. ( a u. { y } ) Q .|| ( F ` x ) <-> ( E. x e. a Q .|| ( F ` x ) \/ E. x e. { y } Q .|| ( F ` x ) ) )
124 122 123 sylibr 
 |-  ( ( ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) /\ ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) ) /\ Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) ) -> E. x e. ( a u. { y } ) Q .|| ( F ` x ) )
125 124 exp31 
 |-  ( ( ( ph /\ a C_ ( F supp .1. ) ) /\ y e. ( ( F supp .1. ) \ a ) ) -> ( ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) -> ( Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) -> E. x e. ( a u. { y } ) Q .|| ( F ` x ) ) ) )
126 125 anasss 
 |-  ( ( ph /\ ( a C_ ( F supp .1. ) /\ y e. ( ( F supp .1. ) \ a ) ) ) -> ( ( Q .|| ( M gsum ( F |` a ) ) -> E. x e. a Q .|| ( F ` x ) ) -> ( Q .|| ( M gsum ( F |` ( a u. { y } ) ) ) -> E. x e. ( a u. { y } ) Q .|| ( F ` x ) ) ) )
127 57 62 67 72 81 126 100 findcard2d 
 |-  ( ph -> ( Q .|| ( M gsum ( F |` ( F supp .1. ) ) ) -> E. x e. ( F supp .1. ) Q .|| ( F ` x ) ) )
128 52 127 mpd 
 |-  ( ph -> E. x e. ( F supp .1. ) Q .|| ( F ` x ) )